CoSim-CPS

1st Workshop on Formal Co-Simulation of Cyber-Physical Systems

A satellite event of SEFM2017

September 5, 2017, Trento, Italy

News

AIMS

This workshop focuses on the integrated application of formal methods and co-simulation technologies in the development of software for Cyber-Physical Systems. Co-simulation is an advanced simulation technique that allows developers to generate a global simulation of a complex system by orchestrating and composing the concurrent simulation of individual components or aspects of the system. Formal methods link software specifications and program code to logic theories, providing developers with means to analyze program behaviors in a way that is demonstrably exhaustive. The two technologies complement each other. Using co-simulation, developers can create prototypes suitable to validate hypotheses embedded in formal models and formal properties to be analyzed of the software. This is fundamental to ensure that the right system is being developed. Using formal methods, developers can extend test results obtained with co-simulation runs, and ensure that the same results apply to all program states for all possible program inputs. This enables early detection of latent design anomalies. This workshop will give researchers and industrial practitioners a stage to demonstrate new methods and tools, present experience reports, discuss open challenges, and explore ideas for future development of frameworks integrating formal methods and co-simulation. Contributions are welcome on all aspects of system development, including specification, design, analysis, implementation and documentation of software for Cyber-Physical Systems.

TOPICS

The proposed workshop aims to give researchers and industrial practitioners a stage to demonstrate new methods and tools, present experience reports, discuss open challenges, and explore ideas for future development of frameworks integrating formal methods and co-simulation. Contributions are welcome on all aspects of system development, including specification, design, analysis, implementation and documentation of software for CPS.

Topics of interest include, but are not limited to, the following:

  • Development of new co-simulation methods and tools
  • Integration of formal methods technologies in co-simulation methods and tools
  • Experience reports on using existing co-simulation methods and tools
  • Emerging standards for co-simulation
  • Modeling and analysis of safety properties of cyber-physical systems
  • Modeling and analysis of human-machine interfaces in cyber-physical systems
  • Modeling and analysis of security aspects of cyber-physical systems
  • Next-Generation cyber-physical systems

INVITED SPEAKER

Claudio Gonçalves Gomes, University of Antwerp

Co-simulation: State of the Art

Abstract. It is essential to find new ways of enabling experts in different disciplines to collaborate more efficiently in the development of ever more complex systems, under increasing market pressures. One possible solution for this challenge is to use a heterogeneous model-based approach where different teams can produce their conventional models and carry out their usual mono-disciplinary analysis, but in addition, the different models can be coupled for simulation (co-simulation), allowing the study of the global behavior of the system. Due to its potential, co-simulation is being studied in many different disciplines but with limited sharing of findings. The aim of this talk is to summarize, bridge, and enhance future research in this multidisciplinary area. We will introduce the main concepts in co-simulation, and survey some of the currently open challenges.

ACCEPTED PAPERS

The following papers will be presented at the workshop. Presentations will last approx 30 minutes (including questions). The detailed schedule will be available soon.

  • Features of Integrated Model-based Co-modelling and Co-simulation Technology [ pdf ] (P.G. Larsen, J. Fitzgerald, J. Woodcock, C. Gamble, R. Payne and K. Pierce)
  • Co-Simulation between Trnsys and Simulink based on Type155 [ pdf ] (G. Engel, A.S. Chakkaravarthy and G. Schweiger)
  • A Framework for Analyzing Adaptive Autonomous Aerial Vehicles [ pdf ] (I.A. Mason, V. Nigam, C. Talcott and A.V. Brito)
  • Co-simulation of semi-autonomous systems: the Line Follower Robot case study [ pdf ] (M. Palmieri, C. Bernardeschi and P. Masci)
  • Development of a Driverless Lawn Mower using Co-Simulation [ pdf ] (F. Foldager, P.G. Larsen and O. Green)
  • A Tool Integration Language to Formalize Co-simulation Tool-chains for Cyber-Physical System [ pdf ] (L. Jinzhi, M. Torngren, D. Chen and W. Jian)
  • Integrated simulation and formal verification of a simple autonomous vehicle [ pdf ] (A. Domenici, A. Fagiolini and M. Palmieri)
  • Injecting Formal Verification in FMI-based Co-Simulations of Cyber-Physical Systems [ pdf ] (L.D. Couto, S. Basagiannis, E.H. Ridouane, A. El-Din Mady, M. Hasanagic and P.G. Larsen)
  • A Refinement Approach to Analyse Critical Cyber-Physical Systems [ pdf ] (D. Basile, F. Di Giandomenico and S. Gnesi)
  • Formalising Cosimulation Models [ pdf ] (F. Zeyda, J. Ouy, S. Foster and A. Cavalcanti)
  • A framework for the co-simulation of engine controls and task scheduling [ pdf ] (P. Pazzaglia, G. Buttazzo and M. Di Natale)
  • Towards Resilience-Explicit Modelling and Co-simulation of Cyber-Physical Systems [ pdf ] (M. Jackson and J. Fitzgerald)
  • Approximated Stability Analysis of Bi-Modal Hybrid Co-simulation Scenarios [ pdf ] (C. Gomes, P. Karalis, E. Navarro-López and H. Vangheluwe)


PROGRAM

  • 8:15 - 9:00 Registration
  • 9:00 - 9:05 Introduction to the workshop
  • 9:05 - 9:55 Keynote: Co-simulation: State of the Art [slides] (Claudio G. Gomes)

Coffee Break (9:55 - 10:25)

  • 10:25 - 10:50 Features of Integrated Model-based Co-modelling and Co-simulation Technology [slides] (P.G. Larsen, J. Fitzgerald, J. Woodcock, C. Gamble, R. Payne and K. Pierce)
  • 10:50 - 11:15 Co-Simulation between Trnsys and Simulink based on Type155 [slides] (G. Engel, A.S. Chakkaravarthy and G. Schweiger)
  • 11:15 - 11:40 A Framework for Analyzing Adaptive Autonomous Aerial Vehicles [slides] (I.A. Mason, V. Nigam, C. Talcott and A.V. Brito)
  • 11:40 - 12:05 Co-simulation of semi-autonomous systems: the Line Follower Robot case study [slides] (M. Palmieri, C. Bernardeschi and P. Masci)
  • 12:05 - 12:30 Development of a Driverless Lawn Mower using Co-Simulation [slides] (F. Foldager, P.G. Larsen and O. Green)

Lunch (12:30 - 14:00)

  • 14:00 - 14:25 A Tool Integration Language to Formalize Co-simulation Tool-chains for Cyber-Physical System [slides] (L. Jinzhi, M. Torngren, D. Chen and W. Jian)
  • 14:25 - 14:50 Integrated simulation and formal verification of a simple autonomous vehicle [slides] (A. Domenici, A. Fagiolini and M. Palmieri)
  • 14:50 - 15:15 Injecting Formal Verification in FMI-based Co-Simulations of Cyber-Physical Systems (L.D. Couto, S. Basagiannis, E.H. Ridouane, A. El-Din Mady, M. Hasanagic and P.G. Larsen)
  • 15:15 - 15:40 A Refinement Approach to Analyse Critical Cyber-Physical Systems [slides] (D. Basile, F. Di Giandomenico and S. Gnesi)
  • 15:40 - 16:05 Formalising Cosimulation Models [slides] (F. Zeyda, J. Ouy, S. Foster and A. Cavalcanti)

Coffee Break (16:05 - 16:30)

  • 16:30 - 16:55 A framework for the co-simulation of engine controls and task scheduling (P. Pazzaglia, G. Buttazzo and M. Di Natale)
  • 16:55 - 17:20 Towards Resilience-Explicit Modelling and Co-simulation of Cyber-Physical Systems [slides] (M. Jackson and J. Fitzgerald)
  • 17:20 - 17:45 Approximated Stability Analysis of Bi-Modal Hybrid Co-simulation Scenarios [slides] (C. Gomes, P. Karalis, E. Navarro-López and H. Vangheluwe)

Closing Remarks

IMPORTANT DATES

  • Abstract submission: June 12, 2017
  • Paper submission: June 19, 2017
  • Notification: July 5, 2017
  • Camera ready: July 31, 2017
  • Workshop: Sep 5, 2017

SUBMISSION GUIDELINES & PROCEEDINGS

Papers can be submitted through Easychair: https://easychair.org/conferences/?conf=cosimcps17

Authors are invited to submit the following types of contributions:

  • Full research papers describing original research results, case studies and tools (up to 15 pages LNCS format, including references)
  • Short papers describing new approaches, techniques and/or tools that are not fully validated yet (up to 6 pages LNCS format, including references)

Papers must describe original contributions whose main results and conclusions have not been published or submitted elsewhere. All papers will be peer-reviewed by at least two members of the program committee.

Accepted papers will be published in the LNCS proceeding volume for SEFM co-located events.

PC CO-CHAIRS

  • Cinzia Bernardeschi, University of Pisa, Italy, cinzia (dot) bernardeschi (at) iet (dot) unipi (dot) it
  • Paolo Masci, INESC TEC and Universidade do Minho, Portugal, paolo (dot) masci (at) inesctec (dot) pt
  • Peter Gorm Larsen, Aarhus University, Denmark, pgl (at) eng (dot) au (dot) dk

PROGRAM COMMITTEE

  • Stylianos Basagiannis, United Technologies Research Center
  • Estela Bicho Erlhagen, Centro Algoritmi / Universidade do Minho
  • David Broman, KTH Royal Institute of Technology
  • Fabio Cremona, United Technologies Research Center
  • Marco Di Natale, Sant'Anna School of Advanced Studies
  • Andrea Domenici, University of Pisa
  • Adriano Fagiolini, University of Palermo
  • Camille Fayollas, IRIT / University of Toulouse 3
  • John Fitzgerald, Newcastle University
  • Stefania Gnesi, ISTI/CNR
  • Temesghen Kahsai, NASA Ames / Carnegie Mellon University
  • Mario Porrmann, Bielefeld University
  • Akshay Rajhans, MathWorks
  • Steve Reeves, University of Waikato
  • Matteo Rossi, Polytechnic University of Milan
  • Sriram Sankaranarayanan, University of Colorado at Boulder
  • Mirko Sessa, Fondazione Bruno Kessler
  • Neeraj Kumar Singh, IRIT-INPT-ENSEEIHT / University of Toulouse
  • Hans Vangheluwe, University of Antwerp / McGill University
  • Yi Zhang, Center for Devices and Radiological Health, US Food and Drug Administration (CDRH/FDA)