nach oben

2015 | Buch

Kapitel lesen Erstes Kapitel lesen

Formal Aspects of Component Software

11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers

herausgegeben von: Ivan Lanese, Eric Madelaine

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

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

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes revised selected papers from the International Symposium on Formal Aspects of Component Software, FACS 2014, held in Bertinoro, Italy, in September 2014.

The 20 full papers presented in this volume were carefully reviewed and selected from 44 submissions. They are organized in topical sections named: compositional approaches; adaptation and evolution; application and experience; tools; scheduling, time and hybrid systems; other verification approaches and safety and liveness of composition. The volume also contains two invited talks, one full paper and one abstract.

Inhaltsverzeichnis

Frontmatter

Invited Speakers

Frontmatter

Components as Location Graphs

Abstract

This paper presents a process calculus framework for modeling ubiquitous computing systems and dynamic component-based structures as location graphs. A key aspect of the framework is its ability to model nested locations with sharing, while allowing the dynamic reconfiguration of the location graph, and the dynamic update of located processes.

Jean-Bernard Stefani

A Formal Approach to Autonomic Systems Programming: The SCEL Language

(Long Abstract)

Abstract

Software-intensive cyber-physical systems have to deal with massive numbers of components, featuring complex interactions among components and with humans and other systems. Often, they are designed to operate in open and non-deterministic environments, and to dynamically adapt to new requirements, technologies and external conditions. This class of systems has been named ensembles and new engineering techniques are needed to address the challenges of developing, integrating, and deploying them. In the paper, we briefly introduce SCEL (Software Component Ensemble Language), a kernel language that takes a holistic approach to programming autonomic computing systems and aims at providing programmers with a complete set of linguistic abstractions for programming the behavior of autonomic components and the formation of autonomic components ensembles, and for controlling the interaction among different components.

Rocco De Nicola

Compositional Approaches

Frontmatter

Verified Service Compositions by Template-Based Construction

Abstract

Today, service compositions often need to be assembled or changed on-the-fly, which leaves only little time for quality assurance. Moreover, quality assurance is complicated by service providers only giving information on their services in terms of domain specific concepts with only limited semantic meaning.

In this paper, we propose a method to construct service compositions based on pre-verified templates. Templates, given as workflow descriptions, are typed over a (domain-independent) template ontology defining concepts and predicates. Templates are proven correct using an abstract semantics, leaving the specific meaning of ontology concepts open, however, only up to given ontology rules. Construction of service compositions amounts to instantiation of templates with domain-specific services. Correctness of an instantiation can then simply be checked by verifying that the domain ontology (a) adheres to the rules of the template ontology, and (b) fulfills the constraints of the employed template.

Sven Walther, Heike Wehrheim

Compositional Verification of Asynchronously Communicating Systems

Abstract

Within a network of asynchronously communicating systems, the complete network is often not known, or even available at run-time. Consequently, verifying whether the network of communicating systems behaves correctly, i.e., the network does not contain any deadlock or livelock, is impracticable. As such systems are highly concurrent by nature, Petri nets form a natural choice to model these systems and their communication.

This paper presents a formal framework based on a generic communication condition to verify correctness of the system by pairwise checking whether these systems communicate correctly and fulfill some condition, then the whole network is guaranteed to behave correctly. As an example, this paper presents the elastic communication condition.

Jan Martijn E. M. van der Werf

Compositional Analysis Using Component-Oriented Interpolation

Abstract

We present a novel abstraction technique that exploits the compositionality of a concurrent system consisting of interacting components. It uses, given an invariant and a component of interest, bounded model checking (BMC) to quickly interpolate an abstraction of that component’s environment. The abstraction may be refined by increasing the BMC bound. Furthermore, it is only defined over variables shared between the component and its environment, resulting in an aggressive abstraction with several applications. We demonstrate its use in a verification setting, as we report on our open source implementation in the NuSMV model checker which was used to perform a practical assessment with industrially-sized models from satellite case studies of ongoing missions. These models are expressed in a formalized dialect of the component-oriented and industrially standardized Architecture Analysis and Design Language (AADL).

Viet Yen Nguyen, Benjamin Bittner, Joost-Pieter Katoen, Thomas Noll

Adaptation and Evolution

Frontmatter

Impact Models for Architecture-Based Self-adaptive Systems

Abstract

Self-adaptive systems have the ability to adapt their behavior to dynamic operation conditions. In reaction to changes in the environment, these systems determine the appropriate corrective actions based in part on information about which action will have the best impact on the system. Existing models used to describe the impact of adaptations are either unable to capture the underlying uncertainty and variability of such dynamic environments, or are not compositional and described at a level of abstraction too low to scale in terms of specification effort required for non-trivial systems. In this paper, we address these shortcomings by describing an approach to the specification of impact models based on architectural system descriptions, which at the same time allows us to represent both variability and uncertainty in the outcome of adaptations, hence improving the selection of the best corrective action. The core of our approach is an impact model language equipped with a formal semantics defined in terms of Discrete Time Markov Chains. To validate our approach, we show how employing our language can improve the accuracy of predictions used for decision-making in the Rainbow framework for architecture-based self-adaptation.

Javier Cámara Moreno, Antónia Lopes, David Garlan, Bradley Schmerl

Decentralised Evaluation of Temporal Patterns over Component-Based Systems at Runtime

Abstract

Self-adaptation allows systems to modify their structure and/or their behaviour depending on the environment and the system itself. Since reconfigurations must not happen at any but in suitable circumstances, guiding and controlling dynamic reconfigurations at runtime is an important issue. This paper contributes to two essential topics of the self-adaptation—a runtime temporal properties evaluation, and a decentralization of control loops. It extends the work on the adaptation of component-based systems at runtime via policies with temporal patterns by providings (a) specific progressive semantics of temporal patterns and (b) a decentralised method which is suitable to deal with temporal patterns of component-based systems at runtime. The implementation with the GROOVE tool constitutes a practical contribution.

Olga Kouchnarenko, Jean-François Weber

Formal Rules for Reliable Component-Based Architecture Evolution

Abstract

Software architectures are the blueprint of software systems construction and evolution. During the overall software lifecycle, several changes of its architecture may be considered (e.g. including new software requirements, correcting bugs, enhancing software performance). To ensure a valid and reliable evolution, software architecture changes must be captured, verified and validated at an early stage of the software evolution process. In this paper, we address this issue by proposing a set of evolution rules for software architectures in a manner that preserves consistency and coherence between abstraction levels. The rules are specified in the B formal language and applied to a three-level Adl that covers the three steps of software development: specification, implementation and deployment. To validate our rules, the approach is tested on a running example of Home Automation Software.

Abderrahman Mokni, Marianne Huchard, Christelle Urtado, Sylvain Vauttier, Huaxi (Yulin) Zhang

Application and Experience

Frontmatter

Solving Parity Games in Scala

Abstract

Parity games are two-player games, played on directed graphs, whose nodes are labeled with priorities. Along a play, the maximal priority occurring infinitely often determines the winner. In the last two decades, a variety of algorithms and successive optimizations have been proposed. The majority of them have been implemented in PGSolver, written in OCaml, which has been elected by the community as the de facto platform to solve efficiently parity games as well as evaluate their performance in several specific cases.

PGSolver includes the Zielonka Recursive Algorithm that has been shown to perform better than the others in randomly generated games. However, even for arenas with a few thousand of nodes (especially over dense graphs), it requires minutes to solve the corresponding game.

In this paper, we deeply revisit the implementation of the recursive algorithm introducing several improvements and making use of Scala Programming Language. These choices have been proved to be very successful, gaining up to two orders of magnitude in running time.

Antonio Di Stasio, Aniello Murano, Vincenzo Prignano, Loredana Sorrentino

Synthesis of a Reconfiguration Service for Mixed-Criticality Multi-Core Systems: An Experience Report

Abstract

Task-level reconfiguration techniques in automotive applications aim to reallocate tasks to computation cores during failures to guarantee that the desired functionality is still delivered. We consider a class of mixed-criticality asymmetric multi-core systems inspired by our collaboration with a leading automotive manufacturing company, for which we automatically synthesize task-level reconfiguration services to reduce the number of processing cores and decrease the cost without weakening fault-tolerance. We admit the following types of faults: safety violations by tasks, permanent core failures, and temporary core failures. We use timed games to synthesize the controllers. The services suspend and reinstate the periodic executions of the non-critical tasks to ensure enough processing capacity for the critical tasks by maintaining lookup tables, which keep track of processing capacity. We present a methodology to synthesize the services and use a case study to show that suitable abstractions can dramatically improve the scalability of timed games-based tools for solving industrial problems.

Md Tawhid Bin Waez, Andrzej Wąsowski, Juergen Dingel, Karen Rudie

Tools

Frontmatter

From Helena Ensemble Specifications to Executable Code

Abstract

The Helena approach [5] provides a modeling technique for distributed systems where components dynamically collaborate in ensembles. Models of such systems are formalized with ensemble specifications. They can be implemented using the jHelena framework [6]. In this paper, we present a domain-specific language for ensemble specifications and provide an Eclipse plug-in featuring an editor and an automatic code generator for translating ensemble specifications into executable code.

Annabelle Klarl, Lucia Cichella, Rolf Hennicker

MAccS: A Tool for Reachability by Design

Abstract

MAccS is a tool for the modular design of complex IT systems. Component specifications are given in the form of marked acceptance specifications which are acceptance specifications, an extension of modal specifications, enriched with reachability constraints on states. The tool supports the crucial operators for a complete specification theory: satisfaction checking, consistency, refinement, product, quotient and conjunction. These operators can be used to build larger systems by composing or decomposing component specifications while ensuring some reachability properties.

Guillaume Verdier, Jean-Baptiste Raclet

MPass: An Efficient Tool for the Analysis of Message-Passing Programs

Abstract

MPass is a freely available open source tool for the verification of message passing programs communicating in an asynchronous manner over unbounded channels. The verification task is non-trivial as it involves exploring state spaces of arbitrary or even infinite sizes. Even for programs that only manipulate finite range variables, the size of the channels could grow unboundedly, and hence the state space that need to be explored could be of infinite size. MPass addresses the bounded-phase reachability problem, where each process is allowed to perform a bounded number of phases during any run of the system. In each phase, a process can perform either send transitions or receive transitions (but not both). However, this does not bound the number of context switches between processes or the size of the channels but just the number of alternations between receive and send transitions of each process. Currently, MPass can decide bounded-phase reachability problem for three types of channel semantics, namely lossy, stuttering and unordered channels. Messages inside these channels can be lost, duplicated and re-arranged, respectively. MPass efficiently and uniformly reduces the bounded-phase reachability problem into the satisfiability of quantifier-free Presburger formula for each of the above mentioned semantics.

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Jonathan Cederberg, Subham Modi, Othmane Rezine, Gaurav Saini

Scheduling, Time, and Hybrid Systems

Frontmatter

Widening the Schedulability of Hierarchical Scheduling Systems

Abstract

This paper presents a compositional approach for schedulability analysis of hierarchical systems, which enables to prove more systems schedulable by having richer and more detailed scheduling models. We use a lightweight method (statistical model checking) for design exploration, easily assuring high confidence in the correctness of the model. A satisfactory design can be proved schedulable using the computation costly method (symbolic model checking). In order to analyze a hierarchical scheduling system compositionally, we introduce the notion of a stochastic supplier modeling the supply of resources in each component. We specifically investigate two different techniques to widen the set of provably schedulable systems: (1) a new supplier model; (2) restricting the potential task offsets. We also provide a way to estimate the minimum resource supply (budget) that a component is required to provide.

Abdeldjalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim Guldstrand Larsen, Marius Mikučionis, Ulrik Nyman, Arne Skou

Adding Formal Meanings to AADL with Hybrid Annex

Abstract

AADL is a Model-Based Engineering language for architectural analysis and specification of real-time embedded systems with stringent performance requirements (e.g. fault-tolerance, security, safety-critical etc.). However, core AADL lacks of a mechanism for modeling continuous evolution of physical processes which are controlled by digital controllers. In our previous work, we have introduced Hybrid Annex—an AADL extension for continuous behavior and cyber-physical interaction modeling based on Hybrid Communicating Sequential Processes (HCSP). In this paper, we present formal semantics of the synchronous subset of AADL models annotated with Hybrid Annex specifications using HCSP. The semantics are then used to verify correctness of AADL models (with Hybrid Annex specifications) using an in-house developed theorem prover — Hybrid Hoare Logic (HHL) prover.

Ehsan Ahmad, Yunwei Dong, Shuling Wang, Naijun Zhan, Liang Zou

Component-Based Modeling and Observer-Based Verification for Railway Safety-Critical Applications

Abstract

One of the challenges that engineers face, during the development process of safety-critical systems, is the verification of safety application models before implementation. Formalization is important in order to verify that the design meets the specified safety requirements. In this paper, we formally describe the set of transformation rules, which are defined for the automatic transformation of safety application source models to timed automata target models. The source models are based on our domain-specific component model, named SARA, dedicated to SAfety-critical RAilway control applications. The target models are then used for the observer-based verification of safety requirements. This method provides an intuitive way of expressing system properties without requiring a significant knowledge of higher order logic and theorem proving, as required in most of existing approaches. An experimentation over a chosen benchmark at rail-road crossing protection application is shown to highlight the proposed approach.

Marc Sango, Laurence Duchien, Christophe Gransart

Other Verification Approaches

Frontmatter

Intransitive Non-Interference by Unfolding

Abstract

Non-interference characterises the absence of undesired information flows in a computing system, by asking that actions with higher level of confidentiality do not cause any observable effect at the lower levels. In many concrete applications, this requirement is too strict and the abstract model is enriched with some form of downgrading, namely with the possibility of declassifying information, thus allowing for a controlled form of leakage. This paper focuses on BINI (Bisimilarity-based Intransitive non-interference), a formalisation of non-interference with downgrading in the setting of Petri nets. Generalising some previous works, we provide a causal characterisation of BINI in terms of the unfolding semantics, a true concurrent semantics of Petri nets. Building on this, we design an algorithm for checking BINI on safe Petri nets which relies on the construction of suitable complete prefixes of the unfolding. The algorithm is implemented in a prototype tool and some preliminary tests are quite encouraging as they suggest that the management of downgrading does not cause any significant performance decay.

Paolo Baldan, Francesco Burato, Alberto Carraro

Reduction and Abstraction Techniques for BIP

Abstract

Reduction and abstraction techniques have been proposed to address the state space explosion problem in verification. In this paper, we present reduction and abstraction techniques for component-based systems modeled in BIP (Behavior, Interaction and Priority). Given a BIP system consisting of several atomic components, we select two atomic components amenable for reduction and compute their product. The resulting product component typically contains constants and branching bisimilar states. We use constant propagation to reduce the resulting component. Then we use a branching bisimulation abstraction to compute an abstraction of the product component. The presented method is fully implemented and scales to large designs not possible to verify with existing techniques.

Mohamad Noureddine, Mohamad Jaber, Simon Bliudze, Fadi A. Zaraket

Compositionality for Quantitative Specifications

Abstract

We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations.

Uli Fahrenberg, Jan Křetínský, Axel Legay, Louis-Marie Traonouez

Safety and Liveness of Composition

Frontmatter

Algorithmic Verification of Procedural Programs in the Presence of Code Variability

Abstract

We present a generic framework for verifying temporal safety properties of procedural programs that are dynamically or statically configured by replacing, adapting, or adding new components. To deal with such a variability of a program, we require programmers to provide local specifications for its variable components, and verify the global properties by replacing these specifications with maximal models. Our framework is a generalization of a previously developed framework that abstracts from all program data. In this work, we capture program data and thus significantly increase the range of properties that can be verified. Our framework is generic by being parametric on the set of observed program events and their semantics. We separate program structure from the behavior it induces to facilitate independent component specification and verification. We provide tool support for an instantiation of our framework to programs written in a procedural language with pointers as the only datatype.

Siavash Soleimanifard, Dilian Gurov

Place-Liveness of ComSA Applications

Abstract

Interactive scientific visualization applications are based on heterogeneous codes to implement simulation, visualization and interaction parts. These different parts need to be precisely assembled to construct high performance applications allowing efficient interactions. Thanks to their programming paradigm, component-based approaches are suitable to construct this kind of applications. However, building a correct application using this paradigm is a difficult task. Even starting up such an application may be a difficult problem since the composition may lead to deadlocks. This paper defines a sufficient condition that ensures place-liveness of a subclass of FIFO nets. This result is used to provide tools that help a user to analyze his application. Especially, this analysis aims at avoiding deadlocks and starting the application up in a way that ensures its liveness i.e. all its components are active.

Abderrahim Ait Wakrime, Sébastien Limet, Sophie Robert

Admit Your Weakness: Verifying Correctness on TSO Architectures

Abstract

Linearizability has become the standard correctness criterion for fine-grained non-atomic concurrent algorithms, however, most approaches assume a sequentially consistent memory model, which is not always realised in practice. In this paper we study the correctness of concurrent algorithms on a weak memory model: the TSO (Total Store Order) memory model, which is commonly implemented by multicore architectures. Here, linearizability is often too strict, and hence, we prove a weaker criterion, quiescent consistency instead. Like linearizability, quiescent consistency is compositional making it an ideal correctness criterion in a component-based context. We demonstrate how to model a typical concurrent algorithm, seqlock, and prove it quiescent consistent using a simulation-based approach. Previous approaches to proving correctness on TSO architectures have been based on linearizabilty which makes it necessary to modify the algorithm’s high-level requirements. Our approach is the first, to our knowledge, for proving correctness without the need for such a modification.

Graeme Smith, John Derrick, Brijesh Dongol

Backmatter

Titel: Formal Aspects of Component Software
herausgegeben von: Ivan Lanese
Eric Madelaine
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-15317-9
Print ISBN: 978-3-319-15316-2
DOI: https://doi.org/10.1007/978-3-319-15317-9