Autumn school – Serene DISIM

SERENE 2012 Autumn School

September 25-26, 2012
Allied to the Workshop, we will hold a 2-day autumn school for students and early-career researchers. The school is an annual event organized by ERCIM working group on Software Engineering for Resilient Systems.

The aim of 2012 edition of the school is to discuss the main advances in model-driven and formal approaches for ensuring quality and dependability of software-intensive systems.

School Program:

September 25, CNR room 28

9:00-10:30	Alessandro Fantechi (University of Florence, IT) “Model checking approach to verify families of dependable systems” Part 1.
10:30-11:00	Coffee
11:00-12:30	Alessandro Fantechi (University of Florence, IT) “Model checking approach to verify families of dependable systems” Part 2.
12:30 14:00	Lunch
14:00-15:30	Ivan Porres (Abo Akademi University, FI) “Empirical Studies and Experimentation in Model Driven Engineering” Part 1.
15:30-16:00	Coffee
16:00-17:30	Ivan Porres (Abo Akademi University, FI) “Empirical Studies and Experimentation in Model Driven Engineering” Part 2.
17:30-18:00	Questions and answers

September 26, CNR room 28

9:00-10:30	Michael Butler (Computer Science at Southampton, UK) “Abstraction, Refinement and Decomposition for Systems Engineering” Part 1.
10:30-11:00	Coffee
11:00-12:30	Michael Butler (Computer Science at Southampton, UK) “Abstraction, Refinement and Decomposition for Systems Engineering” Part 2.
12:30 14:00	Lunch
14:00-15:30	Marco Bozzano (Fondazione Bruno Kessler, Trento (Italy)) “Formal methods for Model Based Safety Analysis”. Part 1.
15:30-16:00	Coffee
16:00-17:30	Marco Bozzano (Fondazione Bruno Kessler, Trento (Italy)) “Formal methods for Model Based Safety Analysis”. Part 2.
17:30-18:00	Questions and answers

Info about the lectures:

Stefania Gnesi (ISTI-CNR, IT) and Alessandro Fantechi (University of Florence, IT)

(Slides download)

Title: Model checking approach to verify families of dependable systemsAbstract: Modelling variability in product families has been the subject of extensive study in the literature on Software Product Lines, especially that concerning Feature Modelling. In recent years, we have laid the basis for the study of the application of temporal logics to the formal modelling of behavioural variability in product family definitions. A critical point in this formalization is to give
an adequate representation of the elements of the feature model and their relation with the behaviour of the many products that are to be derived from the family. We present a logical framework that is able to deal with variability in product family descriptions. The temporal logic MHML is based on the classical Hennessy–Milner logic with Until and we interpret it over Modal Transition Systems (MTSs). MTSs extend the classical notion of Labelled Transition Systems by distinguishing possible (\emph{may\/}) and required (\emph{must\/}) transitions: these two types of transitions are useful to describe variability in behavioural descriptions of product families. This leads to a novel \emph{deontic\/} interpretation of the classical modal and temporal operators, which allows the expression of both constraints over the products of a family and constraints over their behaviour in a single logical framework. model-checking algorithms to verify MHML formulae as well as a way to derive correct products from a product family description are also discussed.

Biography: Alessandro Fantechi received his Laurea degree in Computer Science at the University of Pisa, Italy, in 1978, achieving in the meanwhile the Diploma di Licenza of the Scuola Normale Superiore. Since 2004 he is Full Professor at the Faculty of Engineering of the University of Florence, where he has been Associate Professor since 1995. Previously, he has been Associate Professor at the University of Pisa since 1992, and Researcher at IEI – CNR since 1983. Alessandro Fantechi’s current research is focused on formal modelling of behavioural variability and on the application of formal verification methods, with particular emphasis on model-checking techniques and on their industrial applications. His research interests have included formal description techniques, temporal logic, distributed systems programming and modeling, applications of natural language understanding to requirement engineering. He has written over eighty papers for international journals and conferences, and has acted as the project team leader within several national and international research projects. He has been involved in the organization of several international conferences, on these themes.Stefania Gnesi is director of research at ISTI-CNR and head of the Formal Methods and Tools Laboratory (http://fmt.isti.cnr.it). Stefania Gnesi’s current research interests include the study and
development of temporal logics and model checking tools for the formal specification and verification of concurrent, distributed and mobile systems, and their applications to safety-critical systems, mobile applications and in the formal modelling of behavioural variability in product family engineering. She has also worked on formal aspects of requirements engineering, with particular emphasis on the formalization of requirements as temporal logic formulae and on the application of Natural Language Processing techniques to the analysis of requirements documents.

Ivan Porres (Abo Akademi University, FI)

Title: Empirical Studies and Experimentation in Model Driven Engineering (Slides download)Abstract: Model Driven Engineering has been proposed as a practical alternative to software development using traditional programming languages with the objective to improve communication between stakeholders, utomate many development tasks and to enable early validation and verification of development artifacts. We will study the main foundations of model driven engineering and review the concepts of modeling languages, metamodeling, model
transformation. Then we will argue that in order to validate and assess many model driven engineering approaches in practice there is a need to perform empirical studies. We will focus on controlled experiments on how can they be used to understand better the effect of different development approaches in the outcomes of software engineering tasks. Finally, we will present an empirical study on how and when the use two different design patterns for UML statecharts can
affect the maintainability of a large telecommunication system.

Biography: Prof. Ivan Porres holds a PhD in Computer Engineering from Åbo Akademi University(2001) and is professor of Software Engineering at this university since 2008. He is the leader of the Software Engineering Laboratory and his research is supported by the Academy of Finland, TEKES and EU. He has published over 80 refereed articles and his current research interests include software design languages and tools, especially domain specific modeling languages, engineering cloud software, software testing and empirical methods ins software engineering research.

Michael Butler (Computer Science at Southampton, UK)

Title: Abstraction, Refinement and Decomposition for Systems Engineering Slides download

Abstract: These lectures will address the key role played by formal modelling and verification in systems engineering. Modelling may be used at all stages of the development process from requirements analysis to system acceptance testing. Formal modelling and verification lead to deeper understanding and higher consistency of specification and design than informal or semi-formal methods. In order to manage system complexity, abstraction, refinement and decomposition of formal models are key methods for structuring the formal modelling effort since they support separation of concerns and layered reasoning. A refinement approach means that models and compositions of models represent different abstraction levels of system design; consistency between abstraction levels is ensured by formal verification.

The lectures will use the Event-B formal modelling language and the associated Rodin toolset for Event-B. Event-B is a state-based formal method for system-level modelling and analysis. The key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify the consistency between refinement levels. The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins. The lectures will be structured as follows:

System abstraction and model refinement
Role of proof and tools in Event-B modelling
Structuring refinement
Decomposing models
Implementing models

Relevant case studies will be used to exemplify the techniques.

KEYWORDS: Set theory, logic, state-based modelling

REFERENCES:

J.-R. Abrial (2012). Modeling in Event-B: System and Software Engineering, Cambridge University Press.

J.-R. Abrial, M. Butler, S. Hallerstede, T.S. Hoang, F. Mehta, L. Voisin (2010). Rodin: An Open Toolset for Modelling and Reasoning in Event-B. International Journal on Software Tools for Technology Transfer (STTT), 12, (6), 447-466. http://eprints.soton.ac.uk/271058/

M. Butler (2009). Decomposition Structures for Event-B. In, Integrated Formal Methods iFM2009, Springer, LNCS 5423 Springer.http://eprints.soton.ac.uk/266965/

M. Butler, D. Yadav (2008). An Incremental Development of the Mondex System in Event-B. Formal Aspects of Computing, 20, (1), 61-77.http://eprints.soton.ac.uk/263346/

A. Edmunds, A. Rezazadeh, M. Butler (2012). Formal modelling for Ada implementations: Tasking Event-B. In, Ada-Europe 2012: 17th International Conference on Reliable Software Technologies, Stockholm, SE, 11 – 15 Jun 2012. http://eprints.soton.ac.uk/335400/

Biography: Michael Butler is a Professor of Computer Science at Southampton. He is internationally recognised as leading in refinement-based formal methods. He holds a PhD (Computation) from the University of Oxford. His research work encompasses applications, tools and methodology for formal methods, especially refinement based method such as B and Event-B. He has made key methodological contributions to the Event-B formal method, especially around model composition and decomposition. He plays a leading role in the development of several tools for B and Event-B especially the Rodin toolset. Butler has a strong track record of collaboration with industry (Siemens, Bosch, Critical Software, SAP, NASA, RailSafe and Space Systems Finland). Butler serves on the PC of many international conferences. He was PC Chair of FM2011, the leading international conference on formal methods. He is a Fellow of the British Computer Society, is Vice-chair of IFIP WG 2.3 Programming Methodology and is on theeditorial boards of the Formal Aspects of Computing and Critical Computer-Based Systems journals.

Marco Bozzano (Fondazione Bruno Kessler, Trento (Italy))

Title: Formal methods for Model Based Safety Analysis (Slides download)

Abstract: Safety critical systems – namely systems whose failure may cause death or injury to people, harm to the environment, or economical losses – are becoming more complex, both in the type of functionality they provide and in the way they interact with the environment. This
increasing complexity requires an adequate increase in the capability of safety engineers to assess system safety, encouraging the adoption of formal techniques. In this lecture I will describe recent work on formal methods techniques for Model Based Safety Analysis (MBSA).
This paradigm is based on the notions of fault injection and automatic model extension, that is, automatic integration of nominal (fault-free) system models with (user-defined) fault models, and the use of formal verification tools to analyze the resulting extended model. I will present techniques, based on symbolic model checking, for the automated generation of artifacts that are typical of safety assessment, such as Fault Trees and FMEA tables, and for the analysis
of FDIR (Fault Detection, Identification and Recovery). I will conclude the lecture with an overview of some widely adopted standards for the certification of safety critical systems, in various domains.

Biography: Marco Bozzano is a senior researcher at Fondazione Bruno Kessler, Trento (Italy). He got a PhD degree in Computer Science from the University of Genova in 2002. His research interests include formal methods, model checking and formal safety assessment. He has coauthored more than 50 papers on these topics, and one book entitled “Design and Safety Assessment of Critical Systems” (Taylor & Francis,2010). He has recently been invited as external expert to SAE ARP 4761 working group on Model Based Safety Analysis.

Contact Information
For more information, please use the contact details below, referring explicitly to the SERENE 2012 Autumn School:

Elena A. Troubitsyna
Åbo Akademi University,
Autumn School Director
Elena.Troubitsyna (at) abo.fi