7:45am On-site registration
8:30am Opening welcome by Enrico Vicario (General Chair) and welcome address by Alberto Tesi (Dean of the University of Florence)
9:00am Keynote: Multi‐Agent Networked Systems with Adversarial Elements.
Tamer Başar (University of Illinois at Urbana-Champaign)
Joint program with QEST

Session: Kronecker and product form methods

  • A Structured Solution Approach for Markov Regenerative Processes. Elvio Gilberto Amparore, Peter Buchholz, Susanna Donatelli.
  • Low-rank tensor methods for communicating Markov processes. Daniel Kressner, Francisco Macedo.
Joint program with QEST
11:00am Coffee break at Ristorante Sabatini

Session: Hybrid systems

  • A statistical approach for computing reachability of non-linear and stochastic dynamical systems. Luca Bortolussi, Guido Sanguinetti.
  • Formal synthesis and validation of inhomogeneous thermostatically controlled loads. Sadegh Esmaeil Zadeh Soudjani, Sebastian Gerwinn, Christian Ellen, Martin Fränzle, Alessandro Abate.
  • Finite abstractions of stochastic Max-Plus-Linear systems. Dieky Adzkiya, Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate.
Joint program with QEST
1:00pm Lunch at Ristorante Sabatini

Session: Mean-field/population analysis

  • Mean-field for performance models with generally distributed-timed transitions. Richard Hayden, Illes Horvath, Miklos Telek.
  • Mean-field approximation and quasi-equilibrium reduction of Markov population models. Luca Bortolussi, Rytis Paškauskas.
  • On performance of Gossip communication in a crowd-sensing scenario. Marcel C. Guenther, Jeremy T. Bradley.

Session: Time Petri Nets

  • Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets. S. Birch, T. Jacobsen, J. Jensen, C. Moesgaard, N. Nørgaard Samuelsen, J. Srba.
  • Time Petri Nets with Dynamic Firing Dates: Semantics and Applications. S. Dal Zilio, L. Fronc, B. Berthomieu, F. Vernadat.
  • Delay-dependent partial order reduction technique for time Petri nets. Hanifa Boucheneb, Kamel Barkaoui, Karim Weslati.
4:00pm Coffee break at Ristorante Sabatini

Session: Models and tools

  • Probabilistic Model Checking of DTMC Models of User Activity Patterns. O. Andrei, M. Calder, M. Higgs, M. Girolami.
  • Performance Comparison of IEEE 802.11 DCF and EDCA for Beaconing in Vehicular Networks. Geert Heijenk, Martijn van Eenennaam, Anne Remke.

Session: Metric Interval Temporal Logic

  • On MITL and alternating timed automata over infinite words. Thomas Brihaye, Gilles Geeraerts, Morgane Estiévenart.
  • Data-driven Statistical Learning of Temporal Logic Properties. Ezio Bartocci, Luca Bortolussi, Guido Sanguinetti.
  • A new GreatSPN GUI for GSPN editing and CSLTA model checking (tool paper). Elvio Gilberto Amparore.
  • The Octave queueing Package (tool paper). Moreno Marzolla.
Joint program with QEST
6:00pm End of sessions. Reception at Villa Bardini will start at 7:00pm (check the directions).

Workshops program: International workshop on the Integration of Safety and Security Engineering (ISSE), DEvelopment, Verification and VAlidation of cRiTical Systems (DEVVARTS), Workshop on Architecting Safety in Collaborative Mobile Systems (ASCoMS).

9:00am Joint program with FORMATS Keynote: The Modeling and Analysis of Mixed-Criticality Systems.
Sanjoy Baruah (University of North Carolina at Chapel Hill)

Session: Simulation

  • A perfect sampling algorithm of random walks with forbidden arcs.
    S. Durand, B. Gaujal, F. Perronnin, J.-M. Vincent.
  • Modelling Replication in NoSQL Datastores.
    Rasha Osman, Pietro Piazzolla.

Session: Hybrid Systems I

  • Combined Global and Local Search for the Falsification of Hybrid Systems. Jan Kuřátko, Stefan Ratschan.
  • Time-Bounded Reachability for Initialized Hybrid Automata with Linear Differential Inclusions and Rectangular Constraints. Nima Roohi, Mahesh Viswanathan.
11:00am Coffee break at Ristorante Sabatini

Session: Queueing, debugging, and tools

  • On queues with general service demands and constant service capacity. H. Bruneel, W. Rogiest, J. Walraevens, S. Wittevrongel.
  • Simulation Debugging and Visualization in the Mobius Modeling Framework. Craig Buchanan, Ken Keefe.
  • Scalar: A distributed benchmarking framework for systematic scalability analysis (tool paper). Thomas Heyman, Davy Preuveneers, Wouter Joosen.
  • Non-Intrusive Scalable Memory Access Tracer (tool paper). Nobuyuki Ohba, Seiji Munetoh, Atsuya Okazaki, Yasunao Katayama.

Session: Hybrid Systems II

  • Weak Singular Hybrid Automata. Umang Mathur, Shankara Narayanan Krishna, Ashutosh Trivedi.
  • Non-Convex Invariants and Urgency Conditions on Linear Hybrid Automata. Stefano Minopoli, Goran Frehse.
  • Anonymized Reachability of Hybrid Automata Networks. Taylor T. Johnson, Sayan Mitra.
1:00pm Lunch at Ristorante Sabatini

Session: Process algebras and equivalencies

  • Probabilistic Programming Process Algebra. Anastasis Georgoulas, Jane Hillston, Dimitrios Milios, Guido Sanguinetti.
  • PALOMA: A Process Algebra for Located Markovian Agents. Cheng Feng, Jane Hillston.
  • On the Discriminating Power of Testing Equivalences for Reactive Probabilistic Systems: Results and Open Problems. Marco Bernardo, Davide Sangiorgi, Valeria Vignudelli.

Session: Contracts

  • Virtual Integration of Real-Time Systems based on Resource Segregation Abstraction. Ingo Stierand, Philipp Reinkemeier, Purandar Bhaduri.
  • Modeling Bitcoin Contracts by Timed Automata. M. Andrychowicz, Stefan Dziembowski, Daniel Malinowski, Łukasz Mazurek.
4:00pm Coffee break at Ristorante Sabatini

Session: Automata and Markov process theory

  • Continuity Properties of Distances for Markov Processes. Radu Mardare, Kim Guldstrand Larsen, Manfred Jaeger, Hua Mao.
  • Deciding the value 1 problem for reachability in 1-clock decision stochastic timed automata. Nathalie Bertrand, Thomas Brihaye, Blaise Genest.
  • Decidable Problems for Unary PFAs. Rohit Chadha, Dileep Kini, Mahesh Viswanathan.
Joint program with QEST
6:00pm End of sessions. Social event at Castello dell'Acciaiolo will start at 7:30pm (check the directions).

Workshops program: Next Generation of System Assurance Approaches for Safety-Critical Systems (SASSUR), Dependable Embedded and Cyber-physical Systems and Systems-of-Systems (DECSoS), Reliability and Security Aspects for Critical Infrastructure Protection (ReSA4CI).

9:00am Joint program with SAFECOMP Keynote: Quantitative safety assessment: experiments and field measurements. Henrique Madeira (University of Coimbra). Joint program with SAFECOMP
10:00am Joint program with SAFECOMP

Session: Fault Injection Techniques

  • A Simulated Fault Injection Framework for Time-Triggered Safety-Critical Embedded Systems. Iban Ayestaran, Carlos F. Nicolas, Jon Perez, Asier Larrucea, Peter Puschner.
  • Rapid Fault-Space Exploration by Evolutionary Pruning. Horst Schirmeier, Christoph Borchert, Olaf Spinczyk.

Session: Verification and Synthesis I

  • Finding Best and Worst Case Execution Times of Systems Using Difference-Bound Matrices. O. Bataineh, M. Reynolds, T. French.
  • Timed Pattern Matching. Dogan Ulus, Thomas Ferrere, Eugene Asarin, Oded Maler.
11:00am Coffee break at Ristorante Sabatini

Session: Applications, theory, and tools

  • A Scalable Approach to the Assessment of Storm Impact in Distributed Automation Power Grids. A. Avritzer, L. Carnevali, L. Happe, A. Koziolek, D.S. Menasché, M. Paolieri, S. Suresh.
  • Compositionality Results for Quantitative Information Flow. Y. Kawamoto, K. Chatzikokolakis, C. Palamidessi.
  • CyberSAGE: A Tool for Automatic Security Assessment of Cyber-Physical Systems (tool paper). An Hoa Vu, N.O. Tippenhauer, B. Chen, D.M. Nicol, Z. Kalbarczyk.
  • Tool demonstrations.
Joint program with QEST

Session: Verification and Synthesis II

  • Verification and Performance Evaluation of Timed Game Strategies. A. David, K.G. Larsen, Z. Zhang, H. Fang.
  • The Power of Proofs: New Algorithms for Timed Automata Model Checking. Peter Fontana, Rance Cleaveland.
1:00pm Lunch at Ristorante Sabatini
2:30pm Keynote: Quantitative Evaluation of Service Dependability in Shared Execution Environments. Samuel Kounev (Universität Würzburg). Joint program with QEST

Session: Probabilistic Model Checking

  • Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains. M.N. Rabe, C.M. Wintersteiger, H. Kugler, B. Yordanov, Y. Hamadi.
  • Accelerating Parametric Probabilistic Verification. N. Jansen, F. Corzilius, M. Volk, R. Wimmer, E. Abraham, J.-P. Katoen, B. Becker.
Joint program with QEST
4:30pm Coffee break at Ristorante Sabatini
5:00pm Joint program with SAFECOMP

Session: Verification & Validation Techniques

  • Safety Validation of Sense and Avoid Algorithms using Simulation and Evolutionary Search. Xueyi Zou, Rob Alexander, John McDermid.
  • Debugging with Timed Automata Mutations. Bernhard K. Aichernig, Klaus Hörmaier, Florian Lorber.
Joint program with SAFECOMP
6:00pm End of sessions. End of sessions. Reception at Harry's Bar will start at 7:30pm. End of sessions.

8:30am On-site registration On-site registration
9:00am Keynote: Quantitative Model Checking for Analysis and Repair of Stochastic Control Policies. Armando Tacchella (University of Genoa). Keynote: Key Challenges for the Automotive Industry and Renault. Philippe Quere (Renault). Welcome (9:45am)

Session: Cloud Performance Modeling

  • Optimal Hiring of Cloud Servers. Andrew Stephen Mcgough, Isi Mitrani.
  • Performance evaluation of NoSQL databases. Andrea Gandini, Marco Gribaudo, William Knottenbelt, Rasha Osman, Pietro Piazzolla.

Session: Automotive Systems I

  • Systematic Derivation of Functional Safety Requirements for Automotive Systems. Kristian Beckers, Isabelle Cote, Thomas Frese, Denis Hatebur, Maritta Heisel.
  • Making Implicit Safety Requirements Explicit: An AUTOSAR Safety Case. Thomas Arts, Michele Dorigatti, S. Tonetta.


20 years past and (hopefully) 20 years to come: my experience in Ansaldo STS with formal methods and railways.
Pietro Marmo (Ansaldo STS).

11:00am Coffee break at Ristorante Sabatini

Session: Queuing and Fluid Models

  • A Systematic Approach for Composing General Middleware Completions to Performance Models. Adnan Faisal, Dorina Petriu, Murray Woodside.
  • Vacation and polling models with retrials. Onno Boxma, Jacques Resing.
  • Fluid vacation model with Markov modulated load and exhaustive discipline. Zsolt Saffer, Miklos Telek.


Software Quality, Dependability and Safety in Embedded Systems.
Philip Koopman (Carnegie Mellon University).

Session: Cyber-physical systems

  • Formal verication of steady-state errors in unity-feedback control systems. Muhammad Ahmad, Osman Hasan.
  • Assertion-based monitoring in practice: checking correctness of an automotive DSI3 sensor interface. T. Nguyen, D. Nickovic.
  • Analysis of real-time properties of a digital hydraulic power management system. P. Boström, P. Alexeev, M. Heikkilä, M. Huova, M. Waldén, M. Linjama.

Session: Automotive Systems II

  • Securing Vehicle Diagnostics in Repair Shops. Pierre Kleberger, Tomas Olovsson.
1:00pm Lunch at Ristorante Sabatini

Session: Performance of Computation and Programming

  • Use of a Levy Distribution for Modeling Best Case Execution Time Variation. Jonathan Beard, Roger Chamberlain.
  • On the Predictive Properties of Performance Models Derived Through Input-Output Relationships. Mahmoud Awad, Daniel Menasce.
  • Deriving Work Plans for Solving Performance and Scalability Problems. Christoph Heger, Robert Heinrich.
European Workshop on
Industrial Computer Systems

Session: Computer Networks

  • Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip. Z. Zhang, W. Serwe, J. Wu, T. Yoneda, H. Zheng, C. Myers.
  • Formal Specification and Verification of TCP Extended with the Window Scale Option. L. Lockefeer, D. Williams, W. Fokkink.
  • Learning Fragments of the TCP Communication Protocol. Paul Fiterau Brostean, Ramon Janssen, Frits Vaandrager.

Session: Coverage Models and Mitigation Techniques

  • Analysis of Persistence of Relevance in Systems with Imperfect Fault Coverage. J. Xiang, F. Machida, K. Tadano, Y. Maeno.
  • Exploiting Narrow Data-width to Mask Soft Errors in Register Files. Jianjun Xu, Qingping Tan, Zeming Shao, Hong Ning.
4:00pm Coffee break at Ristorante Sabatini

Session: Fitting

  • Dealing with Zero Density Using Piecewise Phase-type Approximation. Lubos Korenciak, Jan Krcal, Vojtech Rehak.
  • Uncertainty in On-The-Fly Epidemic Fitting. Roxana Danila, Marily Nika, Thomas Wilding, William Knottenbelt.
  • Automated Capacity Planning for PEPA Models. Jane Hillston, Christopher D. Williams.

Session: Assurance cases and arguments

  • Towards a Clearer Understanding of Context and Its Role in Assurance Argument Confidence. Patrick Graydon.
  • Assurance Cases for Block-configurable Software. R. Hawkins, A. Miyazawa, A. Cavalcanti, T. Kelly, J. Rowlands.
  • Generation of Safety Case Argument-Fragments from Safety Contracts. I. Sljivo, B. Gallina, J. Carlson, H. Hansson.

Session: Railway Control Systems

  • On the Validation of an Interlocking System by Model-Checking. Andrea Bonacchi, Alessandro Fantechi.
  • Deadlock Avoidance in Train Scheduling: a Model Checking Approach. F. Mazzanti, G. Oronzo Spagnolo, S. Della Longa, A. Ferrari.
6:00pm End of sessions. Guided tour in the historic city center will start at 7:30pm; dinner at Ristorante Il Latini will start at 8:30pm. End of sessions. Dinner at Ristorante Palazzo Gaddi (Hotel Astoria) will start at 8:00pm. End of sessions. Guided tour in the historic city center will start at 7:30pm; dinner at Ristorante Il Latini will start at 8:30pm.

9:00am Keynote: Machine Learning meets Stochastic Model Checking. Luca Bortolussi (University of Trieste). Keynote: Cyber-Physical Systems in Horizon 2020 - Trends in EU research and innovation activities. Werner Steinhoegl (European Commission).

Session: Urban Traffic Modeling

  • Performance Modeling of Intelligent Car Parking Systems. Karoly Farkas, Gabor Horvath, Andras Meszaros, Miklos Telek.
  • Formal punctuality analysis of frequent bus services using headway data. Daniel Reijsbergen, Stephen Gilmore.

Session: System Analysis

  • Estimating worst case failure dependency with partial knowledge of the difficulty function. Peter Bishop, Lorenzo Strigini.
  • Proving the Absence of Stack Overflows. Daniel Kästner, Christian Ferdinand.


Quantitative Verification: Formal Guarantees for Timeliness, Reliability and Performance.
David Parker (University of Birmingham).

11:00am Coffee break at Ristorante Sabatini

Session: Decision Making

  • Markov decision process and linear programming based control of MAP/MAP/N queues. Andras Meszaros, Miklos Telek.
  • A Decision Making Model of Influencing Behavior in Information Security. Iryna Yevseyeva, Charles Morisset, Thomas Gross, Aad van Moorsel.

Session: Security and Trust

  • Trust-Based Intrusion Tolerant Routing in Wireless Sensor Networks. F. Buccafurri, L. Coppolino, S. D’Antonio, A. Garofalo, G. Lax, A. Nocera, L. Romano.
  • A Petri Net Pattern-oriented approach for the Design of Physical Protection Systems. F. Flammini, U. Gentile, S. Marrone, R. Nardone, V. Vittorini.
  • On two models of noninterference: Rushby and Greve, Wilding, and Vanfleet. A. Garcia Ramirez, J. Schmaltz, F. Verbeek, B. Langenstein, H. Blasum.

Session: Verification Methods

  • An Open Alternative for SMT-based Verification of SCADE Models. Henning Basold, Henning Günther, Michaela Huhn, Stefan Milius.
  • Improving Static Analyses of C Programs with Conditional Predicates. Sandrine Blazy, David Bühler, Boris Yakobowski.
  • Detecting Consistencies and Inconsistencies of Pattern-based Functional Requirements. Christian Ellen, Sven Sieverding, Hardi Hungar.
1:00pm Lunch at Ristorante Sabatini

Session: Markovian Models, Above and Beyond

  • Stochastic Approximation of Global Reachability Probabilities of Markov Population Models. Luca Bortolussi, Roberta Lanciani.
  • Explicit State Space and Markov Chain Generation Using Decision Diagrams. Junaid Babar, Andrew Miner.
  • Non-Markovian Modeling of a Blade Center Chassis Midplane. Salvatore Distefano, Francesco Longo, Marco Scarpa, Kishor Trivedi.

Session: Notations/Languages for safety-related aspects

  • Specifying Safety Monitors for Autonomous Systems using Model-checking. M. Machin, F. Dufossé, J.-P. Blanquart, J. Guiochet, D. Powell, H. Waeselynck.
  • Automatically Generated Safety Mechanisms from Semi-Formal Software Safety Requirements. R. Fonte Boa Trindade, Lukas Bulwahn, Christoph Ainhauser.
  • Querying Safety Cases. Ewen Denney, Dwight Naylor, Ganesh Pai.

Session: Testing

  • Randomised testing of a microprocessor model using SMT-solver state generation. Brian Campbell, Ian Stark.
  • Test Specification Patterns for the Automatic Generation of Test Sequences. Ugo Gentile, Stefano Marrone, Gianluca Mele, Roberto Nardone, Adriano Peron.

FMICS Closing (3:30pm — 3:45pm)

FMICS WG Meeting (3:45pm — 4:30pm)

4:00pm Coffee break at Ristorante Sabatini

Session: Safety and Security

  • Security Application of Failure Mode and Effect Analysis. C. Schmittner, T. Gruber, P. Puschner, E. Schoitsch.
  • Safety and security interactions modeling using the BDMP formalism: case study of a pipeline. S. Kriaa, M. Bouissou, F. Colin, Y. Halgand, L. Pietre-Cambacedes.
  • A Pragmatic Approach towards Safe and Secure Medical Device Integration. Christoph Woskowski.
6:00pm End of sessions.