Program

Thursday, 11th September 2014

10:00 am – Keynote
- Pietro Marmo (Ansaldo STS). 20 years past and (hopefully) 20 years to come: my experience in Ansaldo STS with formal methods and railways.
  Replaced by: Radu Mateescu (Inria). Mu-calculus fragments adequate with divergence-sensitive branching bisimilarity.

11:30 am – Session: Cyber-physical systems
- Muhammad Ahmad, Osman Hasan. Formal verication of steady-state errors in unity-feedback control systems.
- Thang Nguyen, Dejan Nickovic. Assertion-based monitoring in practice: checking correctness of an automotive DSI3 sensor interface.
- Pontus Boström, Petr Alexeev, Mikko Heikkilä, Mikko Huova, Marina Waldén, Matti Linjama. Analysis of real-time properties of a digital hydraulic power management system.

2:30 pm – Session: Computer Networks
- Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng, Chris Myers. Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip.
- Lars Lockefeer, David Williams and Wan Fokkink. Formal Specification and Verification of TCP Extended with the Window Scale Option.
- Paul Fiterau Brostean, Ramon Janssen, Frits Vaandrager. Learning Fragments of the TCP Communication Protocol.

4:30 pm – Session: Railway Control Systems
- Andrea Bonacchi, Alessandro Fantechi. On the Validation of an Interlocking System by Model-Checking.
- Franco Mazzanti, Giorgio Oronzo Spagnolo, Simone Della Longa and Alessio Ferrari. Deadlock Avoidance in Train Scheduling: a Model Checking Approach.

10:00 am – Keynote
- David Parker (University of Birmingham). Quantitative Verification: Formal Guarantees for Timeliness, Reliability and Performance.

11:30 am – Session: Verification Methods
- Henning Basold, Henning Günther, Michaela Huhn, Stefan Milius. An Open Alternative for SMT-based Verification of SCADE Models.
- Sandrine Blazy, David Bühler, Boris Yakobowski. Improving Static Analyses of C Programs with Conditional Predicates.
- Christian Ellen, Sven Sieverding, Hardi Hungar. Detecting Consistencies and Inconsistencies of Pattern-based Functional Requirements.

2:30 – Session: Testing
- Brian Campbell, Ian Stark. Randomised testing of a microprocessor model using SMT-solver state generation.
- Ugo Gentile, Stefano Marrone, Gianluca Mele, Roberto Nardone. Test Specification Patterns for the Automatic Generation of Test Sequences.