IDEA4CPS 2nd General Meeting

On 21-23 November 2012, the second General Meeting of the Sino-Danish Basic Research Center IDEA4CPS took place at East China Normal University, 3663 Zhongshan Road (North).

Program:

Wednesday, November 21

9:30~11:00
Registration and Individual Scientific Discussions

11:30~13:00
Lunch

13:00~13:15
Opening and welcome by Kim Larsen and Huibiao Zhu

13:15~14:00
Kim G Larsen: Statistical Refinement and Model Checking of Stochastic Hybrid Automata (prefer 45 min) (Chair: Huibiao Zhu)

14:00~15:30
Validation and Analysis Techniques 1 (Chair: Jian Zhang)
Dehui Du: An Evaluation Framework for Energy Aware Buildings using Statistical Model Checking

Alexandre David: Optimizing Control Strategies using Statistical Model Checking

Yu Zhang: VeriTrace: Towards Automatic Testing and Verification of Concurrent Programs

15:30~16:00
Photo and Coffee Break

16:00~17:30
Specification and Modeling Formalisms 1 (Chair: Ender Yuksel)
Nicola Dragoni: Energy-Harvesting Wireless Sensor Networks

Danny B Poulsen: Modelling Energy Aware Sensor Network in Uppaal (preliminary work)

Xiaofeng Wu: Linking Operational Semantics and Algebraic Semantics for Wireless Networks

18:00
Dinner

Thursday, November 22

8:45~10:00
Specification and Modeling Formalisms 2 (Chair: Kim G Larsen)
Radu Mardare: Approximate reasoning for Markov processes

Huibiao Zhu: Denotational Semantics for a Probabilistic Timed Shared-Variable Language (prefers 45 min)

10:00~10:30
Coffee Break

10:30~12:00
Mini Cases / Protocols 1 (Chair: Arne Skou)
Ender Yuksel: Smart Grid Security: A Smart Meter-Centric Perspective

Hongli Yang: Performance Analysis of Data Gathering Protocol using PRISM

Huixing Fang: Formal Verification and Simulation: Co-Verification for Subway Control Systems

12:00~13:30
Lunch

13:30~14:45
Cross-level Property Preservation (Chair: Radu Mardare)
Guangyuan Li: Translating Metric Temporal Logic $MTL_{0,\infty}$ into Timed Büchi Automata

Wen Su: Formalizing Hybrid Systems with Event-B (prefers 45 min)

14:45~15:00
Coffee Break

15:00~17:00
Board Member Meeting

18:00
Dinner

Friday, November 23

8:45~10:30
Validation and Analysis Techniques 2 (Chair: Alexandre David)
Zhengkui Zhang: Distributed Algorithms for Controller Synthesis (prefers 45 min)

Zheng Wang: Run time verification for Periodic Control Systems

Ting Su: Coverage-driven Testing

10:30~11:00
Coffee Break

11:00~12:00
Specification and Modeling Formalisms 3 (Chair: Nicola Dragoni)
Roberto Vigo: A Calculus for Quality

Geguang Pu: MDM: A Formal Notation for Periodic Control Systems

12:00~13:30
Lunch

13:30~15:30
Tool Prototypes (Chair: Geguang Pu)
Zhiqiang Zhang: Tools for Combinatorial Testing

Mini Cases / Protocols 2
Xi Wu: Modeling and Verifying the Ariadne Protocol Using Process Algebra

Chao Peng: Service Scheduling for Human in the Vehicle

Xiang Wang and Yang Yang: Introduction of IEEE 802 Standards

15:30~16:30
Coffee Break and Individual Scientific Discussions

18:00
Dinner

Photos from Day 1:

dsc_0415

dsc_0419

dsc_0425

dsc_0427

dsc_0443

dsc_0446

dsc_0448

dsc_0453

dsc_0461

dsc_0464

dsc_0497

dsc_0505

dsc_0510

dsc_0519

dsc_0523

dsc_0536

dsc_0538

dsc_0543

dsc_0576

dsc_0586

dsc_0608

dsc_0612

dsc_0626

dsc_0629

Photos from Day 2:

dsc_0433

dsc_0435

dsc_0444

dsc_0454

dsc_0460

dsc_0461

dsc_0465

dsc_0472

dsc_0476

dsc_0486

dsc_0498

dsc_0511

dsc_0521

dsc_0524

dsc_0537

dsc_0564

Photos from Day 3:

dsc_0586

dsc_0588

dsc_0593

dsc_0610

dsc_0620

dsc_0644

dsc_0664

dsc_0673

dsc_0688

dsc_0710

dsc_0715

dsc_0726

dsc_0735

dsc_0744

dsc_0755

dsc_0765

dsc_0768

dsc_0804

dsc_0833

dsc_0843

dsc_0855

dsc_0861

dsc_0870

dsc_0877

dsc_0887

dsc_0897

dsc_0904