Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben

2010 | Buch

A Framework for Reasoning on Component Composition Kapitel lesen Erstes Kapitel lesen

Formal Methods for Components and Objects

8th International Symposium, FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers

herausgegeben von: Frank S. de Boer, Marcello M. Bonsangue, Stefan Hallerstede, Michael Leuschel

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

All modern industries rely on large and complex software systems. In order to construct such large systems in a systematic manner, the focus of the development methodologies has switched in the last two decades from functional to structural issues. Formal methods have been applied successfully to the verification of medium-sized programs in protocol and hardware design. However, their application to the development of large systems requires a greater emphasis on specification, modeling, and validation techniques supporting the concepts of reusability and modifiability, and their implementation in new extensions of existing programming languages like Java. This state-of-the-art survey presents the outcome of the 8th Symposium on Formal Methods for Components and Objects, held in Eindhoven, The Netherlands, in November 2009. The volume contains 17 revised contributions submitted after the symposium by speakers from each of the following European IST projects: the IST-FP6 project BIONETS on biologically inspired services evolution for the pervasive age; the IST-FP7 project COMPAS on compliance-driven models, languages, and architectures for services; the IST-FP6 project CREDO on modelling and analysis of evolutionary structures for distributed services; the IST-FP7 DEPLOY on industrial deployment of advanced system engineering methods for high productivity and dependability; the IST-FP7 project HATS on highly adaptable and trustworthy software using formal methods; the IST-FP7 project INESS on integrated European railway signalling system; the IST-FP7 project MOGENTES on model-based generation of tests for dependable embedded systems; the IST-FP6 project PROTEST on property based testing; and the IST-FP7 project QUASIMODO on quantitative system properties in model-driven-design of embedded systems.

Inhaltsverzeichnis

Frontmatter

The BIONETS Project

A Framework for Reasoning on Component Composition
Abstract
The main characteristics of component models is their strict structure enabling better code reuse. Correctness of component composition is well understood formally but existing works do not allow for mechanised reasoning on composition and component reconfigurations, whereas a mechanical support would improve the confidence in the existing results. This article presents the formalisation in Isabelle/HOL of a component model, focusing on the structure and on basic lemmas to handle component structure. Our objective in this paper is to present the basic constructs, and the corresponding lemmas allowing the proof of properties related to structure of component models and the handling of structure at runtime. We illustrate the expressiveness of our approach by presenting component semantics, and properties on reconfiguration primitives.
Ludovic Henrio, Florian Kammüller, Muhammad Uzair Khan

The COMPAS Project

Verification of Context-Dependent Channel-Based Service Models
Abstract
The paradigms of service-oriented computing and model-driven development are becoming of increasing importance in the field of software engineering. According to these paradigms, new systems are composed with added value from existing stand-alone services to support business processes across organizations. Services comprising a system but originating from various sources need to be coordinated. The Reo coordination language is a state-of-the-art tool supported approach to channel-based coordination. Reo introduces various types of channels which can be composed to build complex connectors to represent various behavioral protocols. This makes Reo suitable for the modeling of service-based business processes. In previous work we presented a framework for model checking data-aware Reo connectors using the mCRL2 toolset. In this paper, we extend this result with a proof of correctness, evaluation of optimization techniques, and support for context-sensitive analysis.
Natallia Kokash, Christian Krause, Erik P. de Vink

The CREDO Project

The Credo Methodology
(Extended Version)
Abstract
This paper is an extended version of the Credo Methodology [16]. Credo offers tools and techniques to model and analyze highly reconfigurable distributed systems. In a previous version we presented an integrated methodology to use the Credo tool suite. Following a compositional, component–based approach to model and analyze distributed systems, we presented a separation of the system into components and the network. A high–level, abstract representation of the dataflow level on the network was given in terms of behavioral interface automata and a detailed model of the components in terms of Creol models. Here we extend the methodology with a detailed model of the network connecting these components. The Vereofy tool set is used to model and analyze the dataflow of the network in detail. The behavioral automata connect the detailed model of the network and the detailed model of the components. We apply the extended methodology to our running example, a peer-to-peer file-sharing system.
Immo Grabe, Mohammad Mahdi Jaghoori, Joachim Klein, Sascha Klüppelholz, Andries Stam, Christel Baier, Tobias Blechmann, Bernhard K. Aichernig, Frank de Boer, Andreas Griesmayer, Einar Broch Johnsen, Marcel Kyas, Wolfgang Leister, Rudolf Schlatte, Martin Steffen, Simon Tschirner, Liang Xuedong, Wang Yi

The DEPLOY Project

Patterns for Refinement Automation
Abstract
Formal modelling is indispensable for engineering highly dependable systems. However, a wider acceptance of formal methods is hindered by their insufficient usability and scalability. In this paper, we aim at assisting developers in rigorous modelling and design by increasing automation of development steps. We introduce a notion of refinement patterns – generic representations of typical correctness-preserving model transformations. Our definition of a refinement pattern contains a description of syntactic model transformations, as well as the pattern applicability conditions and proof obligations for verifying correctness preservation. This work establishes a basis for building a tool that would support formal system development via pattern reuse and instantiation. We present a prototype of such a tool and some examples of refinement patterns for automated development in the Event B formalism.
Alexei Iliasov, Elena Troubitsyna, Linas Laibinis, Alexander Romanovsky
Applying Event-B Atomicity Decomposition to a Multi Media Protocol
Abstract
Atomicity Decomposition is a technique in the Event-B formal method, which augments Event-B refinement with additional structuring in a diagrammatic notation to support complex refinement in Event-B. This paper presents an evaluation of Event-B atomicity decomposition technique in modeling a multi media case study with the diagrammatic notation. Firstly the existing technique and the diagrammatic notation are shown. Secondly an evaluation is performed by developing a model of a Media Channel System. A Media Channel is established between two endpoints for transferring multi-media data. Finally some extensions to the existing diagrammatic notation are proposed and applied to the multi-media case study.
Asieh Salehi Fathabadi, Michael Butler

The FM-SOA Working Group

Abstract Certification of Global Non-interference in Rewriting Logic
Abstract
Non–interference is a semantic program property that assigns confidentiality levels to data objects and prevents illicit information flows from occurring from high to low security levels. In this paper, we present a novel security model for global non–interference which approximates non–interference as a safety property. We also propose a certification technique for global non-interference of complete Java classes based on rewriting logic, a very general logical and semantic framework that is efficiently implemented in the high-level programming language Maude. Starting from an existing Java semantics specification written in Maude, we develop an extended, information–flow Java semantics that allows us to correctly observe global non-interference policies. In order to achieve a finite state transition system, we develop an abstract Java semantics that we use for secure and effective non-interference Java analysis. The analysis produces certificates that are independently checkable and are small enough to be used in practice.
Mauricio Alba-Castro, María Alpuente, Santiago Escobar

The HATS Project

Interleaving Symbolic Execution and Partial Evaluation
Abstract
Partial evaluation is a program specialization technique that allows to optimize programs for which partial input is known. We show that partial evaluation can be used with advantage to speed up as well symbolic execution of programs. Interestingly, the input required for partial evaluation comes from symbolic execution itself which makes it natural to interleave partial evaluation and symbolic execution steps in a software verification setup.
Richard Bubel, Reiner Hähnle, Ran Ji

The INESS Project

The Use of Model Transformation in the INESS Project
Abstract
The INESS (INtegrated European Signalling System) Project is an effort, funded by the FP7 programme of the European Union, to provide a common, integrated, railway signalling system within Europe. It comprises 30 partners, including 6 railway companies. INESS experts have been using the Executable UML (xUML) language to model the proposed integrated signalling system. Because of the safety-critical aspects of these systems, one key idea is to use formal verification techniques to analyse the xUML models for inconsistencies in the requirements and against core properties provided by professional railway engineers. Our objective in the project is to equip our INESS partners with an automated tool to carry out this analysis. Therefore, we have devised a formal verification strategy that uses model transformation technology to automatically translate xUML models to the input language of existing, state-of-the-art, model checking tools. In this paper we describe this formal verification strategy in more detail: we present initial results on implementing the automatic generation of PROMELA models that can be analysed using the SPIN model checker.
Osmar M. dos Santos, Jim Woodcock, Richard F. Paige, Steve King
Suitability of mCRL2 for Concurrent-System Design: A 2 × 2 Switch Case Study
Abstract
Specifying concurrent systems can be done using a variety of languages. These languages have different features and therefore are not necessarily equally suitable for capturing concepts from reality with respect to both expressivity and ease-of-use.
This paper addresses these aspects for the specification language mCRL2 by considering the 2 × 2 Switch case study. This case study has been used before to compare other specification languages, more specifically TLA+, Bluespec, Statecharts and ACP. The case study primarily focuses on two important features, namely multi-party communication and priority of certain actions over other actions. We show that mCRL2 is appropriate for the specification of these features, especially multi-party communication. Moreover, we express some of the requirements of the original case study in terms of modal μ-calculus formulae and establish that these are indeed satisfied by the model.
Frank P. M. Stappers, Michel A. Reniers, Jan Friso Groote

The MOGENTES Project

Mapping UML to Labeled Transition Systems for Test-Case Generation
A Translation via Object-Oriented Action Systems
Abstract
The Unified Modeling Language (UML) is a well known and widely used standard for building software models. While it is familiar to many software engineers, it lacks standardized formal semantics. In this paper, we extend on the formalism of object-oriented action systems (OOAS) and describe a mapping of a selected UML-subset to OOAS by choosing one of the several possible semantics of UML. This mapping, together with the introduction of a trace semantics for OOAS, paves the way for applying tools for and theory of labeled transition systems to UML-models. As a running example, we use a car alarm system in the context of model-based test-case generation and show how the UML mapping is done.
Willibald Krenn, Rupert Schlick, Bernhard K. Aichernig
Mutation-Based Test Case Generation for Simulink Models
Abstract
The Matlab/Simulink language has become the standard formalism for modeling and implementing control software in areas like avionics, automotive, railway, and process automation. Such software is often safety critical, and bugs have potentially disastrous consequences for people and material involved. We define a verification methodology to assess the correctness of Simulink programs by means of automated test-case generation. In the style of fault- and mutation-based testing, the coverage of a Simulink program by a test suite is defined in terms of the detection of injected faults. Using bounded model checking techniques, we are able to effectively and automatically compute test suites for given fault models. Several optimisations are discussed to make the approach practical for realistic Simulink programs and fault models, and to obtain accurate coverage measures.
Angelo Brillout, Nannan He, Michele Mazzucchi, Daniel Kroening, Mitra Purandare, Philipp Rümmer, Georg Weissenbacher
Model-Based Mutation Testing of Hybrid Systems
Abstract
This paper presents a novel model-based testing approach developed in the MOGENTES project. The aim is to test embedded systems controlling a continuous environment, i.e., hybrid systems. We present our two key abstractions against which we systematically test for conformance. (1) Classical action systems are used to model the discrete controller behavior. (2) Qualitative differential equations are used to model the evolutions of the environment. The latter is based on a technique from the domain of Artificial Intelligence called qualitative reasoning. Mutation testing on these models is used to generate effective test cases. A test case generator has been developed that searches for all test cases that would kill a mutant. The mutant models represent our fault models. The generated test cases are then executed on the implementation in order to systematically exclude the possibility that a mutant has been implemented.
Bernhard K. Aichernig, Harald Brandl, Elisabeth Jöbstl, Willibald Krenn

The PROTEST Project

Property-Based Testing - The ProTest Project
Abstract
The ProTest project is an FP7 STREP on property based testing. The purpose of the project is to develop software engineering approaches to improve reliability of service-oriented networks; support fault-finding and diagnosis based on specified properties of the system. And to do so we will build automated tools that will generate and run tests, monitor execution at run-time, and log events for analysis.
The Erlang / Open Telecom Platform has been chosen as our initial implementation vehicle due to its robustness and reliability within the telecoms sector. It is noted for its success in the ATM telecoms switches by Ericsson, one of the project partners, as well as for multiple other uses such as in facebook, yahoo etc. In this paper we provide an overview of the project goals, as well as detailing initial progress in developing property based testing techniques and tools for the concurrent functional programming language Erlang.
John Derrick, Neil Walkinshaw, Thomas Arts, Clara Benac Earle, Francesco Cesarini, Lars-Ake Fredlund, Victor Gulias, John Hughes, Simon Thompson
Incrementally Discovering Testable Specifications from Program Executions
Abstract
The ProTest project is an EU FP7 project to develop techniques that improve the testing and verification of concurrent and distributed software systems. One of the four main work packages is concerned with the automated identification of specifications that could serve as a suitable basis for testing; this is currently a tedious and error-prone manual task that tends to be neglected in practice. This paper describes how this problem has been addressed in the ProTest project. It describes a technique that uses test executions to refine the specification from which they are generated. It shows how the technique has been implemented and applied to real Erlang systems. It also describes in detail the major challenges that remain to be addressed in future work.
Neil Walkinshaw, John Derrick

The QUASIMODO Project

Methodologies for Specification of Real-Time Systems Using Timed I/O Automata
Abstract
We present a real-time specification framework based on Timed I/O Automata and a comprehensive tool support for it. The framework supports various design methodologies including: top-down refinement—for decomposition of abstract specifications towards increasingly detailed models; bottom-up abstraction—for synthesis of complex systems from more concrete models; and step-wise modularisation of requirements—to factor out behaviours given by existing available components from a complex global requirements specification to be implemented. These methodologies are realized by consecutive applications of operators from the following set: refinement, consistency checking, logical and structural composition and quotienting. Additionally, our tool allows combining the component-oriented design process with verification of temporal logic properties increasing the flexibility of the process.
Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, Andrzej Wąsowski
The How and Why of Interactive Markov Chains
Abstract
This paper reviews the model of interactive Markov chains (IMCs, for short), an extension of labelled transition systems with exponentially delayed transitions. We show that IMCs are closed under parallel composition and hiding, and show how IMCs can be compositionally aggregated prior to analysis by e.g., bisimulation minimisation or aggressive abstraction based on simulation pre-congruences. We survey some recent analysis techniques for IMCs, i.e., explaining how measures such as reachability probabilities can be obtained. Finally, we demonstrate that IMCs are a natural (and simple) semantic model for stochastic process algebras and generalised stochastic Petri nets and can be used for engineering formalisms such as AADL and dynamic fault trees.
Holger Hermanns, Joost-Pieter Katoen
Backmatter
Metadaten
Titel
Formal Methods for Components and Objects
herausgegeben von
Frank S. de Boer
Marcello M. Bonsangue
Stefan Hallerstede
Michael Leuschel
Copyright-Jahr
2010
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-17071-3
Print ISBN
978-3-642-17070-6
DOI
https://doi.org/10.1007/978-3-642-17071-3

Premium Partner

    Bildnachweise