Workshop: Applications of Formal Methods and Digital Twins

The model-based concept of a Digital Twin is a new development paradigm in complex systems engineering at the intersection of Cyber-Physical Systems, Software Engineering, System Engineering and Data Science.

While some connections to model-based techniques from formal methods have been recognized in academic contexts, there is no exploitation of this connection in industrial practice. The Workshop on Applications of Formal Methods and Digital Twins will bring together researchers from Formal Methods and practitioners to explore (1) the current challenges in engineering Digital Twins, and (2) the current challenges in applying formal methods to Digital Twins.

The aim of the workshop is to find common ground between industrial needs for model-based engineering of Digital Twins, and Formal Methods. To this end, we welcome the contribution of short papers that will form the foundation for a journal article that illustrates the perspectives, challenges and first applications of Formal Methods in Digital Twins.

Aim and Scope

Topics include, but are not limited to:

  • Applications of FM in Digital Twins
  • Challenges for applying FM in Digital Twins
  • Challenges in Digital Twins that would benefit from applying FM
  • Correctness criteria for Digital Twins
  • Experiences with rigorous engineering of Digital Twins
  • Models for safety and security of Digital Twins
  • Fidelity of Digital Twins
  • Validation of Digital Twins
  • Achievements applying FM to Digital Twins

Submission Guidelines

Submissions are expected to have 6-8 pages in LNCS format. All submitted papers will be refereed by the program committee. Submissions will be handled via EasyChair (https://easychair.org/conferences/?conf=fmdt23).

Important Dates (AoE)

  • Submission: 13.01.23 25.01.23
  • Notification: 17.02.23 24.02.23
  • Final Version: 24.02.23 03.03.23
  • Workshop: 06.03.23

Publication

All accepted articles will be published as informal pre-proceedings and the authors will be invited to contribute to a journal article that positions Formal Methods with respect to Digital Twins, targeting a journal such as Formal Aspects of Computing.

Program Committee

  • Stefan Hallerstede, Aarhus University, DK, co-chair
  • Eduard Kamburjan, University of Oslo, NO, co-chair
  • Stylianos Basagiannis, Collins Airspace, US
  • Loek Cleophas, TU Eindhoven, NL
  • Fuyuki Ishikawa, NII, JP
  • Regine Laleau, Université Paris-Est Créteil, FR
  • Tiziana Margaria, University of Limerick, IE
  • Danielle Stewart, Galois Inc., USA
  • Mahsa Varshosaz, IT, DK
  • Manuel Wimmer, JKU Linz, AU
  • Jim Woodcock, University of York, UK

Program

You can find the preproceedings here (link will be moved later)

  • 09:00 Welcome
  • 09:15 Invited Speaker: Ana Cavalcanti RoboStar Twins?
    • The RoboStar framework for Software Engineering for Robotics has not been created with Digital Twinning in mind. It provides, however, a rich collection of domain-specific notations, with precise mathematical semantics, and associated techniques for automatic generation of simulations and tests. The highly modular approach adopted in developing RoboStar models and simulations is useful to address the reality gap by revealing and recording the structure and the assumptions of the robotic system. In this presentation, we describe the RoboStar modelling stack and the RoboStar approach to testing. Can the use of these techniques be useful in the construction of a digital shadow or twin? We welcome the views of the workshop attendees.
  • 10:15 Break
  • 11:00 Leveraging Runtime Verification for the Monitoring of Digital Twins
    Sylvain Hallé, Chukri Soueidi and Yliès Falcone
  • 11:30 Emerging Challenges in Compositionality and Correctness for Digital Twins
    Eduard Kamburjan, Vidar Klungre, Silvia Lizeth Tapia Tarifa, Rudolf Schlatte, Martin Giese, David Cameron and Einar Broch Johnsen
  • 12:00 Are Formal Contracts a useful Digital Twin of Software Systems?
    Jonas Schiffl and Alexander Weigl
  • 12:30 Lunch
  • 14:00 Digital Twin for Rescue Missions – a Case Study
    Martin Leucker, Martin Sachenbacher and Lars Bernd Vosteen
  • 14:30 A Digital Twin for Coupling Mobility and Energy Optimization: The ReNuBiL Living Lab
    Daniel Thoma, Martin Sachenbacher, Martin Leucker and Aliyu Tanko Ali
  • 15:00 Mining Digital Twins of a VPN Server
    Andrea Pferscher, Benjamin Wunderling, Bernhard K. Aichernig and Edi Muskardin
  • 15:30 Coffee Break
  • 16:00 Discussion