Program
MoDeVVa will take place on October 3rd in Västerås, Sweden.
Keynote Speaker: Prof. Ciprian TEODOROV (Lab-STICC, ENSTA Bretagne)
The Boundary Between Executable Specification Languages and Behavior Analysis Tools
The formal verification community strives to prove the correctness of a specification using formal logic and mathematical proofs. The tremendous progress in computer-aided formal verification tools, along with an ever-growing number of success stories renders these methods essential in the system designer toolbox. However, with the advent of domain-specific models and languages, many formalisms are proposed for writing dynamic system specifications, each one adapted to the specific needs of the targeted domain. A new question emerges: How to bridge the gap between these domain-specific formalisms, geared toward domain experts, and the formal verification tools, geared towards mathematicians?
One of the answers, ubiquitous in the literature, relies on using model transformations to translate the domain-specific model to the verification model syntactically. We argue that this approach is counterproductive leading to semantic multiplication, which requires equivalence proofs that can be hard to provide and maintain. In the talk, I will present a new semantic-level answer developed, refined, and evaluated during the last 10 years. The core building block of this approach is a language-agnostic semantic-level interface, which acts as a bridge between the dynamic semantics of a domain-specific language and the behavior analysis tools.
Short bio: Ciprian Teodorov is full professor at ENSTA Bretagne in Brest, France. Ciprian is a member of the Processes for Safe and Secure Software and Systems (P4S) team of the Lab-STICC Laboratory. His main research interests are the industrialization of formal verification techniques for complex system validation. Ciprian leads the OBP2 Semantic Diagnosis & Formal Verification research team. Since 2013, Ciprian focused on the design of a compositional software architecture that eases the creation of domain-specific verification tools. In 2023, Ciprian received the habilitation (HDR) from the University Western Brittany, Brest, France. In the past, he worked as an EDA/CAD Software engineer at Dolphin Integration (now Dolphin Design) in Meylan, France. Ciprian received his Ph.D. in Computer Science from the University of Western Brittany in 2011, for his work on model-driven physical design for emerging computing architectures.
Full-day detailed program
8:45 - 10:00 : Welcome and Keynote Talk
Workshop opening
Keynote by Prof. Ciprian TEODOROV: The Boundary Between Executable Specification Languages and Behavior Analysis Tools
10:00 - 10:30 : Break
10:30 - 12:00 : Session 1. Chair: Jérôme Hugues
Baptiste Gueuziec, Jean-Pierre Gallois and Frédéric Boulanger.
Qualitative Reasoning and Cyber-Physical Systems: Abstraction, Modeling and Optimized SimulationSebastian Ebert, Johannes Mey, René Schöne, Sebastian Götz and Uwe Assmann.
DiNeROS: A Model-Driven Framework for Verifiable ROS Applications with Petri NetsRakshit Mittal, Raheleh Eslampanah, Lucas Lima, Hans Vangheluwe and Dominique Blouin.
Towards an Ontological Framework for Validity Frames (short paper)
12:00 - 13:30 : Lunch Break
13:30 - 15:00 : Session 2. Chair: Dominique Blouin
David Delgado, Lola Burgueño, Javier Cámara and Javier Troya.
Towards an Extensible Architecture and Tool Support for Model-based Verification (short paper)Matthias Pasquier, Ciprian Teodorov, Frédéric Jouault, Matthias Brun and Loic Lagadec.
Debugging Paxos in the UML MultiverseMario Fuksa, Sandro Speth and Steffen Becker.
Applicability of the ViMoTest Approach for Automated GUI Testing: A Field Study
15:00 - 15:30 : Break
15:30 - 17:00 : Session 3. Chair: Iulian Ober
Alexander Lauer, Jens Kosiol and Gabriele Taentzer.
Empowering model repair: A rule-based approach to graph repair without side effectsAntonio Rosales and Mustafa Al Lail.
Automated Mitigation of Frame Problem in UML Class Diagram VerificationDiscussion and wrap-up