You are here: HomeABZ 2016Invited Talks

Invited Talks

Comparing Abstract State Machine Models with Petri Nets for Distributed Algorithms

Egon Börger

       

Presenter
Egon Börger, Department of Computer Science, University of Pisa, Italy

Bio
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.

Abstract
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 concurrent ASMs.

Atelier B Has Turned Twenty

Thierry Lecomte

       

Presenter
Thierry Lecomte, Clearsy, France

Bio
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).

Abstract
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

       

Presenter
Klaus Reichl, Thales Ground Transport Division, Austria

Bio
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 1986. 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 LinkedIn and GooglePlus.

Abstract
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 model.

How to Brew Your Own Hybrid/Cyberphysical Formalism

Richard Banach

       

Presenter
Richard Banach, School of Computer Science, University of Manchester, UK

Bio
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.

Abstract
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.