|Comparing Abstract State Machine Models with Petri Nets
for Distributed Algorithms
Presenter Egon Börger, Department of Computer
Science, University of Pisa, Italy
Studies of philosophy, logic and mathematics in Paris (Sorbonne), Louvain
(Belgium) and Münster (Germany) 1965-1971. Doctoral degree (1971), Habilitation
(1976), Dozent in mathematics 1976-1978 at University of Münster. Professor
in computer science at University of Salerno (Italy) 1972-1976, Dortmund (Germany)
1978-1985, Udine (Italy) 1982/83 and since 1985 Pisa (Italy). Sabbaticals spent
at IBM, Siemens, Microsoft, SAP, ETH Zürich. (Co)Author of five books and of
over 100 research papers in logic and computer science. Current research interest
in rigorous methods and their industrial application for the design and the
analysis of hardware/software systems. Humboldt Research Award 2007/2014,
Festschrift LNCS 5115/7316/7321, member of Academia Europaea.
We compare some characteristic Petri net models
for distributed algorithms with equivalent Abstract State Machines.
The comparison reveals a certain number of ideosyncrasies of Petri
nets which tend to unnecessarily complicate both the model design
and the analysis of system properties. We indicate how one can avoid
such framework related technicalities by generalizing Petri nets to
|Atelier B Has Turned Twenty
Thierry Lecomte, Clearsy, France
R&D Director at ClearSy, involved in the
development of Atelier B since 1995, with a focus on proof
and code generation (C, LLVM, VHDL).
In this talk, we give an historical account of the
development and industrial applications of Atelier B during the last twenty
years and tentatively draw a picture of the next twenty years.
|Modeling Safety Critical Railway Applications - an Industrial Experience
Klaus Reichl, Thales
Ground Transport Division, Austria
Klaus Reichl is a Senior System and Software Architect at Thales
Ground Transport Division in charge of engineering highest quality
solutions in the safety critical area of railway applications.
He received his master degree from Vienna University of Technology in
After the development of fault tolerant, real-time computation and
communication platforms in the late 1990s, he has been entering the
core business development of train signalling and is currently
enganged in architecting and modeling signalling applications.
In his spare time, he loves playing guitar, indoor and outdoor, and is
hiking and skiing the mountains, mostly outdoor.
Klaus can be found on
The presentation gives an overview on the vision of modeling for
railway applications and a feedback to the current state of the art in
the railway domain. We will show requirements to methodologies and
tools for modeling and reasoning together with objectives and
goals. These stem from industrial needs towards sustainable product
developement beyond use cases discussed in the formal methods area.
Traditionally, essential parts of railway funtionality are related to
safety critical control and thus need to undergo rigorous reasoning
(hard facts about the product). This process is guided by the CENELEC
normatives, which highly recomment the use of formal methods.
Moreover, we discuss aspects like modularity, large-scale reuse,
composability and variability (hard facts about the developement of
the product and the relation to the products properties).
Addressing the problems above, we introduce a common domain model to
ensure the consistency of viewpoints for different aspects on the same
|How to Brew Your Own Hybrid/Cyberphysical Formalism
Richard Banach, School of Computer Science,
University of Manchester, UK
Richard Banach received a Ph.D. in Theoretical Physics, in 1979
from Manchester University. In 1982 he joined ICL, working on the ICL 3980 mainframe.
In 1986 he joined Manchester University Computer Science Department working with the
Alvey Flagship Project, subsequently becoming more concerned with the theory of graph
rewriting. More recently he became interested in the development of formal system models
towards implementation, particularly in situations in which there were awkward requirements.
(Examples include large real world applications, and engineering applications which start
from a continuous physical model.) Most recently, these interests have expanded to focus on
hybrid and cyberphysical systems, especially critical ones, where the broader focus on correctness
issues has proved beneficial. This has led to the development of Hybrid Event-B, a methodology for
the top-down development of cyberphysical systems.
We outline a `requirements-led' approach to designing a
foundational framework for hybrid and cyberphysical systems, where the requirements
come from giving equal weight to computing formalisms, physical modelling approaches,
and the various branches of mathematics that underpin these disciplines. Guiding this
process are the way that discrete event formalisms relate to real world behaviour, and
the deep analogies that exist between discrete event transitions and descriptions of
continuous behaviour. Further considerations affect notions of refinement for such
formalisms. Existing formalisms for modelling features of cyberphysical systems can
be seen as partial projections of the fuller picture.