Powered by
Conference Publishing Consulting

2012 First International Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA), June 2, 2012, Zurich, Switzerland

FormSERA 2012 – Proceedings

Contents - Abstracts - Authors

First International Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA)


Title Page

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

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.
Article Search
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.
Article Search


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.
Article Search
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.
Article Search
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.
Article Search


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.

Article Search
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.
Article Search
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.
Article Search

Real-Time and Round-Table

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.
Article Search

proc time: 0.02