Program

Time QEST FORMATS
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
10:00am

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
11:30am

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
2:30pm

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
4:30pm

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.
5:30pm
  • 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).

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

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
11:30am

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
2:30pm

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
4:30pm

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).

Time QEST SAFECOMP FORMATS
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
11:30am

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
3:30pm

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.

Time EPEW SAFECOMP FMICS
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)
10:00am

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.

Keynote

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
11:30am

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.

Keynote

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.
12:30am

Session: Automotive Systems II

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

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.
3:00pm

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
4:30pm

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.
5:30pm
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.

Time EPEW SAFECOMP FMICS
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).
10:00am

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.

Keynote

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

11:00am Coffee break at Ristorante Sabatini
11:30am

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
2:30pm

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
4:30pm

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.