Powered by
2012 First International Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA),
June 2, 2012,
Zurich, Switzerland
First International Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA)
Preface
Foreword
The workshop addresses the use formal methods in software development practice. Formal methods differ from many software engineering techniques in that they demand and exploit a mathematically rigorous semantic basis for the tools and notations used. Such sound foundations permit the analysis of software engineering artifacts to a depth, and with a degree of automation, that is
otherwise impossible to achieve.
Ample studies show that formal techniques can be used in industrial settings, given careful and tool-supported application. However, the maturing of formal techniques into real-life software engineering involves providing notations and tools that are readily understood and used by practitioners, and the integration of such tools with activities that are far from the unrealistic assumptions that characterized some earlier research in formal methods. Examples include deployment of formal methods in conjunction with structured requirements analysis and modeling, programming practices, test technology, aspect-oriented techniques and agile development practices.
Invited Talk and Best Paper
(Chair: Nico Plat)
Formalisms and Structures (Keynote Abstract)
Michael Jackson
(Open University, UK; University of Newcastle, UK)
Two fundamental pillars of Software Engineering practice are formalism and structure. Formalism allows engineers to reason rigorously about the system in hand; structure allows them to understand its purposes and behaviours. In the constructive activity of system development structure must therefore take precedence. The central role of formalism is to check and verify -- or, where necessary, correct --the products of more informal modes of thought.
In this talk these ideas are explored in the context of an illustrative system. The large structure of the system functionality is discussed, together with the nature of the components of that structure. Informal criteria of functional simplicity are presented. The inescapable mismatch between an intelligible functional structure and implementable software architecture is exposed. The role of formalism in these concerns is suggested.
@InProceedings{FormSERA12p1,
author = {Michael Jackson},
title = {Formalisms and Structures (Keynote Abstract)},
booktitle = {Proc.\ FormSERA},
publisher = {IEEE},
pages = {1--1},
doi = {},
year = {2012},
}
Further Steps Towards Efficient Runtime Verification: Handling Probabilistic Cost Models
Antonio Filieri and Carlo Ghezzi
(Politecnico di Milano, Italy)
We consider high-level models that specify system behaviors probabilistically and support the specification of cost attributes. Specifically, we focus on Discrete Time Markov Reward Models (D-MRMs), i.e. state machines where probabilities can be associated with transitions and rewards (costs) can be associated with states and transitions. Through probabilities we model assumptions on the behavior of environment in which an application is embedded. Rewards can instead model the cost assumptions involved in the system's operations. A system is designed to satisfy the requirements, under the given assumptions. Design-time assumptions, however, can turn out to be invalid at runtime, and therefore it is necessary to verify whether changes may lead to requirements violations. If they do, it is necessary to adapt the behavior in a self-healing manner to continue to satisfy the requirements.
We have previously presented an approach to support efficient runtime probabilistic model checking of DTMCs for properties expressed in PCTL. In this paper we extend the approach to D-MRMs and reward properties. The benefits of the approach are justified both theoretically and empirically on significant test cases.
@InProceedings{FormSERA12p2,
author = {Antonio Filieri and Carlo Ghezzi},
title = {Further Steps Towards Efficient Runtime Verification: Handling Probabilistic Cost Models},
booktitle = {Proc.\ FormSERA},
publisher = {IEEE},
pages = {2--8},
doi = {},
year = {2012},
}
Process
(Chair: Stefan Gruner)
Language Engineering as an Enabler for Incrementally Defined Formal Analyses
Daniel Ratiu, Bernhard Schätz, Markus Voelter, and Bernd Kolb
(fortiss, Germany; itemis, Germany)
There is a big semantic gap between today's general purpose programming
languages on the one hand and the input languages of formal verification tools
on the other hand. This makes integrating formal analyses into the daily
development practice artificially complex. In this paper we advocate that the
use of language engineering techniques can substantially improve this situation
along three dimensions. First, more abstract and thus more analyzable domain
specific languages can be defined, avoiding the need for abstraction recovery
from programs written in general purpose languages. Second, restrictions on the
use of existing languages can be imposed and thereby more analyzable code can be
obtained and analyses can be incrementally defined. Third, by expressing verification conditions and the verification
results at the domain level, they are easier to define and the results of
analyses are easier to interpret by end users. We exemplify our approach with
three domain specific language fragments integrated into the C programming
language, together with a set of analyses: completeness and consistency of
decision tables, model-checking-based analyses for a dialect of state machines
and consistency of feature models. The examples are based on the mbeddr stack,
an extensible C language and IDE for embedded software development.
@InProceedings{FormSERA12p9,
author = {Daniel Ratiu and Bernhard Schätz and Markus Voelter and Bernd Kolb},
title = {Language Engineering as an Enabler for Incrementally Defined Formal Analyses},
booktitle = {Proc.\ FormSERA},
publisher = {IEEE},
pages = {9--15},
doi = {},
year = {2012},
}
Making Sense of Recursion Patterns
Paul Bailes and Leighton A. Brough
(University of Queensland, Australia)
Recursion patterns (such as “foldr” and elaborations thereof) have the potential to supplant explicit recursion in a viable subrecursive functional style of programming. Especially however in order to be able to eschew explicit recursion entirely, even in the definition of new recursion patterns, it’s essential to identify and validate a minimal set of basic recursion patterns. The immediate plausibility of foldr is validated by its application to the implementation of functions and recursion patterns, and especially by an abstract characterization of the programming devices used in these applications used to overcome complementary information deficiencies in data and control.
@InProceedings{FormSERA12p16,
author = {Paul Bailes and Leighton A. Brough},
title = {Making Sense of Recursion Patterns},
booktitle = {Proc.\ FormSERA},
publisher = {IEEE},
pages = {16--22},
doi = {},
year = {2012},
}
Scrum Goes Formal: Agile Methods for Safety-Critical Systems
Sune Wolff
(Terma A/S, Denmark)
Formal methods have had a relative low penetration in industry but have the potential for much wider use. The use of agile methods has been highly limited in development of safety-critical systems due to the lack of formal evaluation techniques and rigorous planning. A combination of formal methods and agile development processes can potentially widen the use of formal methods in industry as well as enabling the use of agile methods in development of safety-critical systems. This paper describes a way to add the use of formal methods to the agile development process Scrum. Experiences from using a variant of the strategy in an industrial case are summarised.
@InProceedings{FormSERA12p23,
author = {Sune Wolff},
title = {Scrum Goes Formal: Agile Methods for Safety-Critical Systems},
booktitle = {Proc.\ FormSERA},
publisher = {IEEE},
pages = {23--29},
doi = {},
year = {2012},
}
Tools
(Chair: Bernhard Rumpe)
Revisiting Modal Interface Automata
Ivo Krka and
Nenad Medvidović
(University of Southern California, USA)
Modern software systems are typically built of components that communicate through their external interfaces. A component’s behavior can be effectively described using finite state automata-based formalisms (e.g., statecharts []). The basic formalism, labelled transition systems, describes the behavior of a component in terms of states and labeled transitions. The more advanced formalisms, such as modal transition systems and interface automata, extend LTS to incorporate additional information related to interface operation controllability-distinguishing between input, output, and internal actions-and the possible partiality of a component’s specification-distinguishing between required and unknown (maybe) behaviors. Capturing the controllability and partiality aspects of a component’s specification facilitates (1) checking interface compatibility, (2) checking whether one component can safely replace another component, and (3) checking whether one specification is a proper refinement of another specification. In this paper, we study the existing definitions of these three types of checks, and then exemplify their limitations in the context of modal interface automata (MIA); MIA is a class of component behavior specifications that incorporates both controllability and partiality information. We outline a set of enhancements to MIA as possible solutions to the identified limitations.
@InProceedings{FormSERA12p30,
author = {Ivo Krka and Nenad Medvidović},
title = {Revisiting Modal Interface Automata},
booktitle = {Proc.\ FormSERA},
publisher = {IEEE},
pages = {30--36},
doi = {},
year = {2012},
}
Automated Continuous Quality Assurance
Johannes Neubauer, Bernhard Steffen, Oliver Bauer, Stephan Windmüller, Maik Merten, Tiziana Margaria, and Falk Howar
(TU Dortmund, Germany; University of Potsdam, Germany)
We present a case study that illustrates the power of active
learning for enabling the automated quality assurance of complex and distributed
evolving systems. We illustrate how the development of the OCS, Springer
Verlag's Online Conference System, is supported by continuous learning-based
testing, that by its nature maintains the synchrony of the running
application and the learned (test) model. The evolution of the test
model clearly indicates which portions of the system remain stable
and which are altered. Thus our approach includes classical regression
testing and feature interaction detection. We show concretely how model
checking, automata learning, and quantitative analysis concur with the holistic
quality assurance of this product.
@InProceedings{FormSERA12p37,
author = {Johannes Neubauer and Bernhard Steffen and Oliver Bauer and Stephan Windmüller and Maik Merten and Tiziana Margaria and Falk Howar},
title = {Automated Continuous Quality Assurance},
booktitle = {Proc.\ FormSERA},
publisher = {IEEE},
pages = {37--43},
doi = {},
year = {2012},
}
EMFtoCSP: A Tool for the Lightweight Verification of EMF Models
Carlos A. González, Fabian Büttner, Robert Clarisó, and Jordi Cabot
(École des Mines de Nantes, France; INRIA, France; LINA, France; Universitat Oberta de Catalunya, Spain)
The increasing popularity of MDE results in the creation of larger models and model transformations, hence converting the specification of MDE artefacts in an error-prone
task. Therefore, mechanisms to ensure quality and absence of errors in models are needed to assure the reliability of the MDE-based development process. Formal methods have proven their worth in the verification of software and hardware systems. However, the adoption of formal methods as a valid
alternative to ensure model correctness is compromised for the inner complexity of the problem. To circumvent this complexity, it is common to impose limitations such as reducing the type of constructs that can appear in the model, or turning the verification process from automatic into user assisted. Since we consider these limitations to be counterproductive for the adoption of formal methods, in this paper we present EMFtoCSP, a new tool for the fully automatic, decidable and
expressive verification of EMF models that uses constraint logic programming as the underlying formalism.
@InProceedings{FormSERA12p44,
author = {Carlos A. González and Fabian Büttner and Robert Clarisó and Jordi Cabot},
title = {EMFtoCSP: A Tool for the Lightweight Verification of EMF Models},
booktitle = {Proc.\ FormSERA},
publisher = {IEEE},
pages = {44--50},
doi = {},
year = {2012},
}
Real-Time and Round-Table
(Chair: Stefania Gnesi)
Augmenting Event-B Modelling with Real-Time Verification
Alexei Iliasov, Alexander Romanovsky, Linas Laibinis, Elena Troubitsyna, and Timo Latvala
(Newcastle University, UK; Åbo Akademi University, Finland; Space Systems Finland, Finland)
A large number of dependable embedded systems have stringent real-time requirements imposed on them. Analysis of their real-time behaviour is usually conducted at the implementation level. However, it is desirable to obtain an evaluation of real-time properties early at the development cycle, i.e., at the modelling stage. In this paper we present an approach to augmenting Event-B modelling with verification of real-time properties in Uppaal. We show how to extract a process-based view from an Event-B model that together with introducing time constraints allows us to obtain a timed automata model – an input model of Uppaal. We illustrate the approach by development and verification of the data processing software of the BepiColombo Mission.
@InProceedings{FormSERA12p51,
author = {Alexei Iliasov and Alexander Romanovsky and Linas Laibinis and Elena Troubitsyna and Timo Latvala},
title = {Augmenting Event-B Modelling with Real-Time Verification},
booktitle = {Proc.\ FormSERA},
publisher = {IEEE},
pages = {51--57},
doi = {},
year = {2012},
}
proc time: 0.09