Update Program.md

.github/src/content/site/2024/Program.md

@@ -87,11 +87,7 @@ skyline:
 <div style='border-bottom: 0.2ex solid gray;'><div style='width:15%; display:inline-block; overflow-wrap: break-word;'>15:00 - 15:30</div><div style='display:inline-block; width:75%;'><details><summary><b>FRETting and Formal Modelling: A Mechanical Lung Ventilator</b></summary>In this paper, we use NASA's Formal Requirements Elicitation Tool (FRET) and the Event-B formal method to model and verify the requirements for the ABZ 2024 case study which is a mechanical lung ventilator. We use the FRET requirements to guide the development of a formal design model in Event-B. We provide details about the artefacts produced and reflect on our experience of using these  tools in this case study. We focus on the functional and controller requirements for this system, as given in the case study documentation. This paper provides a first step towards using Event-B as part of a FRET-guided verification workflow in a large case study.</details><i>Marie Farrell, Matt Luckcuck, Rosemary Monahan, Conor Reynolds, Oisin Sheridan</i></div><div style='width:10%; display:inline-block;'>Case Study</div></div>
 <div style='border-bottom: 0.2ex solid gray; background-color:#e89b26''><div style='width:15%; display:inline-block; overflow-wrap: break-word;'>15:30 - 16:00</div><div style='display:inline-block; width:75%; '><b>Coffee break</b></div><div style='width:10%; display:inline-block;'></div></div>
 <div style='border-bottom: 0.2ex solid gray; background-color:#83a9c6''><div style='display:inline-block; width:75%;'><b>Session Chair: <i>Alexander Raschke</i></b></div></div>
-
 <div style='border-bottom: 0.2ex solid gray;'><div style='width:15%; display:inline-block; overflow-wrap: break-word;'>16:00 - 16:30</div><div style='display:inline-block; width:75%;'><details><summary><b>The Meaning of Self-Modifying Programs for Sequential Machines</b></summary>We propose a definition of a class of reflective Abstract State Machines (ASMs) that extends the class of Parallel Guarded Assignments (PGAs), a subclass of single-agent sequential ASMs, and can serve as ground model for refinements of reflectivity in concrete programming languages.</details><i>Egon Boerger, Vincenzo Gervasi</i></div><div style='width:10%; display:inline-block;'>Theory Extension</div></div>
-<div style='border-bottom: 0.2ex solid gray;'><div style='width:15%; display:inline-block; overflow-wrap: break-word;'>16:00 - 16:30</div><div style='display:inline-block; width:75%;'><details><summary><b>From Concept to Code: Unveiling a Tool for Translating Abstract State Machines into Java Code</b></summary>Formal methods play a crucial role in modeling and quality assurance, but to be deployed on real systems, formal specifications need to be translated into implementation. Manually converting formal models into code poses challenges such as increased costs, limitations in specification reuse, and the potential for introducing errors. To overcome these limitations, Model-Driven Engineering (MDE) approaches enable developers to generate software code automatically. This paper proposes the Asmeta2Java tool for the automatic translation of formal Asmeta specifications into executable Java code. The designers start at an abstract level and perform refinement steps and verification activities. At the end, they automatically generate the code by applying the model-to-code transformation. Moreover, a process to validate and evaluate the transformation is presented.</details><i>Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini</i></div><div style='width:10%; display:inline-block;'>Tools</div></div>
-
-
 <div style='border-bottom: 0.2ex solid gray;'><div style='width:15%; display:inline-block; overflow-wrap: break-word;'>16:30 - 16:45</div><div style='display:inline-block; width:75%;'><details><summary><b>Using Symbolic Execution to Transform Turbo Abstract State Machines into Basic Abstract State Machines</b></summary>This paper introduces a transformation method that uses symbolic execution to eliminate sequential composition (''seq'') rules from turbo ASM rules by translating them into equivalent rules without ''seq''. Under some circumstances ''iterate'' rules can also be eliminated. The material presented here is work in progress. A prototype implementation of the transformation is publicly available.</details><i>Giuseppe Del Castillo</i></div><div style='width:10%; display:inline-block;'>Tools</div></div>
 <div style='border-bottom: 0.2ex solid gray;'><div style='width:15%; display:inline-block; overflow-wrap: break-word;'>16:45 - 17:00</div><div style='display:inline-block; width:75%;'><details><summary><b>Multi-model animation with Jeb</b></summary>A challenge posed by model-based formal methods such as Event-B is the validation of the models. This has been recognized and some tools have been created to provide modelers with means to animate models and to explore their behaviour through graphical display. These tools are quite effective on standalone models but lack the ability to connect to other external models. CPS systems fall under this category, as well as systems built of components interacting through a communication network. In the context of Jeb, an animation tool for Event-B models based on JavaScript, we explore the possibility of connecting models through Websockets. The paper presents a simple protocol to connect simulations. Using an example inspired by  the Lung Ventilator case study, it shows how the implementation expands JeB functionality without modifying its core.</details><i>Jean-Pierre Jacquot</i></div><div style='width:10%; display:inline-block;'>Tools</div></div>
 <div style='border-bottom: 0.2ex solid gray;'><div style='width:15%; display:inline-block; overflow-wrap: break-word;'>17:00 - 17:15</div><div style='display:inline-block; width:75%;'><details><summary><b>Meta-Programming Event-B: Advancing Tool Support and Language Extensions</b></summary>Transforming models based on their textual representation is a cumbersome task. This is particularly the case for Event-B, where the predominant representation is a set of XML files. As a consequence, tool support is lacking, even for minor refactoring operations. The contribution of this paper extends the lisb library with a front and backend based on Event-B. The aim is to bring benefits, that have been demonstrated for classical B, such as an easily transformable data representation of formal specifications as well as creation of custom DSLs and tooling, to Event-B. We see great benefits of such a meta-programming approach for formal specifications and advocate that similar mechanisms will be sensible extensions to the expressiveness of formal methods. Ultimately, our work facilitates language extensions (e.g., re-introducing if-then-else constructs to Event-B which generate multiple events or a proper macro system to avoid code duplication) and tool support (e.g., refactoring tools or automatic refinement).</details><i>Julius Armbrüster, Philipp Körner</i></div><div style='width:10%; display:inline-block;'>Tools</div></div>