Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2017 | Book

Formal Models and Analysis for Self-adaptive Cyber-physical Systems Read chapter Read first chapter

Formal Aspects of Component Software

13th International Conference, FACS 2016, Besançon, France, October 19-21, 2016, Revised Selected Papers

Editors: Olga Kouchnarenko, Ramtin Khosravi

Publisher: Springer International Publishing

Book Series : Lecture Notes in Computer Science

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

This book constitutes the thoroughly revised selected papers from the 13th International Conference on Formal Aspects of Component Software, FACS 2016, held in Besançon, France, in October 2016.

The 11 full papers presented together with one tool paper and 3 invited papers were carefully reviewed and selected from 27 submissions. FACS 2016 is concerned with how formal methods can be used to make component-based and service-oriented software development succeed. Formal methods have provided a foundation for component-based software by successfully addressing challenging issues such as mathematical models for components, composition and adaptation, or rigorous approaches to verification, deployment, testing, and certification.

Table of Contents

Frontmatter

Invited Papers

Frontmatter
Formal Models and Analysis for Self-adaptive Cyber-physical Systems
(Extended Abstract)
Abstract
In this extended abstract, we will analyze the current challenges for the envisioned Self-Adaptive CPS. In addition, we will outline our results to approach these challenges with SMARTSOS [10] a generic approach based on extensions of graph transformation systems employing open and adaptive collaborations and models at runtime for trustworthy self-adaptation, self-organization, and evolution of the individual systems and the system-of-systems level taking the independent development, operation, management, and evolution of these systems into account.
Holger Giese
From Formal Methods to Software Components: Back to the Future?
Abstract
Looking back at the past, I believe Formal Methods and Component-based Software Engineering have missed opportunities to synergise. Looking forward to the future, I believe even more strongly that this synergy will be crucial for developing Software Engineering techniques that tackle scale and complexity. In this position paper I outline the fundamentals of my belief, in terms of existing work and future challenges.
Kung-Kiu Lau

Full Research Papers

Frontmatter
A Core Model for Choreographic Programming
Abstract
Choreographic Programming is a paradigm for developing concurrent programs that are deadlock-free by construction, by programming communications declaratively and then synthesising process implementations automatically. Despite strong interest on choreographies, a foundational model that explains which computations can be performed with the hallmark constructs of choreographies is still missing.
In this work, we introduce Core Choreographies (CC), a model that includes only the core primitives of choreographic programming. Every computable function can be implemented as a choreography in CC, from which we can synthesise a process implementation where independent computations run in parallel. We discuss the design of CC and argue that it constitutes a canonical model for choreographic programming.
Luís Cruz-Filipe, Fabrizio Montesi
Checking Business Process Evolution
Abstract
Business processes support the modeling and the implementation of software as workflows of local and inter-process activities. Taking over structuring and composition, evolution has become a central concern in software development. We advocate it should be taken into account as soon as the modeling of business processes, which can thereafter be made executable using process engines or model-to-code transformations. We show here that business process evolution needs formal analysis in order to compare different versions of processes, identify precisely the differences between them, and ensure the desired consistency. To reach this objective, we first present a model transformation from the BPMN standard notation to the LNT process algebra. We then propose a set of relations for comparing business processes at the formal model level. With reference to related work, we propose a richer set of comparison primitives supporting renaming, refinement, property- and context-awareness. Thanks to an implementation of our approach that can be used through a Web application, we put the checking of evolution within the reach of business process designers.
Pascal Poizat, Gwen Salaün, Ajay Krishna
Compositionality, Decompositionality and Refinement in Input/Output Conformance Testing
Abstract
We propose an input/output conformance testing theory utilizing Modal Interface Automata with Input Refusals (IR-MIA) as novel behavioral formalism for both the specification and the implementation under test. A modal refinement relation on IR-MIA allows distinguishing between obligatory and allowed output behaviors, as well as between implicitly underspecified and explicitly forbidden input behaviors. The theory therefore supports positive and negative conformance testing with optimistic and pessimistic environmental assumptions. We further show that the resulting conformance relation on IR-MIA, called modal-irioco, enjoys many desirable properties concerning component-based behaviors. First, modal-irioco is preserved under modal refinement and constitutes a preorder under certain restrictions which can be ensured by a canonical input completion for IR-MIA. Second, under the same restrictions, modal-irioco is compositional with respect to parallel composition of IR-MIA with multi-cast and hiding. Finally, the quotient operator on IR-MIA, as the inverse to parallel composition, facilitates decompositionality in conformance testing to solve the unknown-component problem.
Lars Luthmann, Stephan Mennicke, Malte Lochau
Checking Multi-view Consistency of Discrete Systems with Respect to Periodic Sampling Abstractions
Abstract
In multi-view modeling the system under development is described by distinct models, called views, which capture different perspectives of the system. Inevitably, possible overlaps of the views may give rise to inconsistencies. Hence, it becomes essential to check for consistency among the separate views. Existing work checks view consistency of discrete systems (transition systems or finite automata) with respect to two types of abstraction functions: (1) projections of state variables, (2) projections of an alphabet of events onto a subalphabet. In this paper, we study view consistency with respect to timing abstractions, specifically, periodic sampling. We define the multi-view consistency problem for periodic sampling abstractions, and provide an algorithm for the problem.
Maria Pittou, Stavros Tripakis
Constrained Synthesis from Component Libraries
Abstract
Synthesis from component libraries is the problem of building a network of components from a given library, such that the network realizes a given specification. This problem is undecidable in general. It becomes decidable if we impose a bound on the number of chosen components. However, the bounded problem remains computationally hard and brute-force approaches do not scale. In this paper we study scalable methods for solving the problem of bounded synthesis from libraries, proposing a solution based on the CounterExample-Guided Inductive Synthesis paradigm. Although our synthesis algorithm does not assume a specific formalism a priori, we present a parallel implementation which instantiates components defined as Linear Temporal Logic-based Assume/Guarantee Contracts. We show the potential of our approach and evaluate our implementation by applying it to an industrial case study.
Antonio Iannopollo, Stavros Tripakis, Alberto Sangiovanni-Vincentelli
MARTE/pCCSL: Modeling and Refining Stochastic Behaviors of CPSs with Probabilistic Logical Clocks
Abstract
Cyber-Physical Systems (CPSs) are networks of heterogeneous embedded systems immersed within a physical environment. Several ad-hoc frameworks and mathematical models have been studied to deal with challenging issues raised by CPSs. In this paper, we explore a more standard-based approach that relies on SysML/MARTE to capture different aspects of CPSs, including structure, behaviors, clock constraints, and non-functional properties. The novelty of our work lies in the use of logical clocks and MARTE/CCSL to drive and coordinate different models. Meanwhile, to capture stochastic behaviors of CPSs, we propose an extension of CCSL, called pCCSL, where logical clocks are adorned with stochastic properties. Possible variants are explored using Statistical Model Checking (SMC) via a transformation from the MARTE/pCCSL models into Stochastic Hybrid Automata. The whole process is illustrated through a case study of energy-aware building, in which the system is modeled by SysML/MARTE/pCCSL and different variants are explored through SMC to help expose the best alternative solutions.
Dehui Du, Ping Huang, Kaiqiang Jiang, Frédéric Mallet, Mingrui Yang
A Formal and Run-Time Framework for the Adaptation of Local Behaviours to Match a Global Property
Abstract
We address the problem of automatically identifying what local properties the agents of a Cyber Physical System have to satisfy to guarantee a global required property \(\phi \). To enrich the picture, we consider properties where, besides qualitative requirements on the actions to be performed, we assume a weight associated with them: quantitative properties are specified through a weighted modal-logic. We propose both a formal machinery based on a Quantitative Partial Model Checking function on contexts, and a run-time machinery that algorithmically tries to check if the local behaviours proposed by the agents satisfy \(\phi \). The proposed approach can be seen as a run-time decomposition, privacy-sensitive in the sense agents do not have to disclose their full behaviour.
Stefano Bistarelli, Fabio Martinelli, Ilaria Matteucci, Francesco Santini
Formal Analysis of Predictable Data Flow in Fault-Tolerant Multicore Systems
Abstract
The need to integrate large and complex functions into today’s vehicle electronic control systems requires high performance computing platforms, while at the same time the manufacturers try to reduce cost, power consumption and ensure safety. Traditionally, safety isolation and fault containment of software tasks have been achieved by either physically or temporally segregating them. This approach is reliable but inefficient in terms of processor utilization. Dynamic approaches that achieve better utilization without sacrificing safety isolation and fault containment appear to be of increasing interest. One of these approaches relies on predictable data flow introduced in PharOS and Giotto. In this paper, we extend the work on leveraging predictable data flow by addressing the problem of how the predictability of data flow can be proved formally for mixed criticality systems that run on multicore platforms and are subject to failures. We consider dynamic tasks where the timing attributes vary from one period to another. Our setting also allows for sporadic deadline overruns and accounts for criticality during fault handling. A user interface was created to allow automatic generation of the models as well as visualization of the analysis results, whereas predictability is verified using the Spin model checker.
Boris Madzar, Jalil Boudjadar, Juergen Dingel, Thomas E. Fuhrman, S. Ramesh
Reasoning About Connectors in Coq
Abstract
Reo is a channel-based exogenous coordination model in which complex coordinators, called connectors, are compositionally built out of simpler ones. In this paper, we present a new approach to model connectors in Coq which is a proof assistant based on higher-order logic and \(\lambda \)-calculus. The model reflects the original structure of connectors simply and clearly. In our framework, basic connectors (channels) are interpreted as axioms and composition operations are specified as inference rules. Furthermore, connectors are interpreted as logical predicates which describe the relation between inputs and outputs. With such definitions provided, connector properties, as well as equivalence and refinement relations between different connectors, can be naturally formalized as goals in Coq and easily proved using pre-defined tactics.
Xiyue Zhang, Weijiang Hong, Yi Li, Meng Sun
(Context-Sensitivity In) Reo, Revisited
Abstract
Coordination languages emerged for programming interaction protocols among components in component-based systems, in terms of connectors. One such language is Reo. Reo facilitates compositional construction of complex composite connectors out of simple primitive ones. Unlike the behavior of connectors in other coordination languages, the behavior of a connector in Reo may depend on whether its coordinated components are ready for https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-57666-4_12/449545_1_En_12_IEq1_HTML.gif . Such behavior is called “context-sensitivity”, and its formalization—a nontrivial problem—has received considerable attention from the community. In this paper, I study three common and historically significant primitives in Reo—context-sensitive LossySync, FIFOn, and LossyFIFOn—and prove that they have inconsistent informal semantics. Moreover, four major formal semantics of Reo do not correspond with its foremost alternative informal semantics.
Sung-Shik T. Q. Jongmans
Validated Test Models for Software Product Lines: Featured Finite State Machines
Abstract
Variants of the finite state machine (FSM) model have been extensively used to describe the behaviour of reactive systems. In particular, several model-based testing techniques have been developed to support test case generation and test case executions from FSMs. Most such techniques require several validation properties to hold for the underlying test models. In this paper, we propose an extension of the FSM test model for software product lines (SPLs), named featured finite state machine (FFSM). As the first step towards using FFSMs as test models, we define feature-oriented variants of basic test model validation criteria. We show how the high-level validation properties coincide with the necessary properties on the product FSMs. Moreover, we provide a mechanised tool prototype for checking the feature-oriented properties using satisfiability modulo theory (SMT) solver tools. We investigate the applicability of our approach by applying it to both randomly generated FFSMs as well as those from a realistic case study (the Body Comfort System). The results of our study show that for random FFSMs over 16 independent non-mandatory features, our technique provides substantial efficiency gains for the set of proposed validity checks.
Vanderson Hafemann Fragal, Adenilso Simao, Mohammad Reza Mousavi

Tool Papers

Frontmatter
Tool Support for Fuzz Testing of Component-Based System Adaptation Policies
Abstract
Self-adaptation enables component-based systems to evolve by means of dynamic reconfigurations that can modify their architecture and/or behaviour at runtime. In this context, we use adaptation policies to trigger reconfigurations that must only happen in suitable circumstances, thus avoiding unwanted behaviours. A tool (cbsdr, standing for Component-Based System Dynamic Reconfigurations) supporting both the Fractal and FraSCAti component frameworks was developed, but the testing of the robustness of new adaptation policies was not easy. This is the reason to add to our implementation a new behavioural fuzzing tool. While fuzzing consists of sending invalid data to a system under test to find weaknesses that may cause a crash or an abnormal reaction, behavioural fuzzing sends invalid sequences of valid data. Valid traces are modified using fuzzing techniques to generate test cases that can be replayed on a dummy system using the adaptation policies to be tested while focusing on interesting regions of specific data sequences.
Jean-François Weber

Applications and Experiences Papers

Frontmatter
Coordinated Actors for Reliable Self-adaptive Systems
Abstract
Self-adaptive systems are systems that automatically adapt in response to environmental and internal changes, such as possible failures and variations in resource availability. Such systems are often realized by a MAPE-K feedback loop, where Monitor, Analyze, Plan and Execute components have access to a runtime model of the system and environment which is kept in the Knowledge component. In order to provide guarantees on the correctness of a self-adaptive system at runtime, the MAPE-K feedback loop needs to be extended with assurance techniques. To address this issue, we propose a coordinated actor-based approach to build a reusable and scalable model@runtime for self-adaptive systems in the domain of track-based traffic control systems. We demonstrate the approach by implementing an automated Air Traffic Control system (ATC) using Ptolemy tool. We compare different adaptation policies on the ATC model based on performance metrics and analyze combination of policies in different configurations of the model. We enriched our framework with runtime performance analysis such that for any unexpected change, subsequent behavior of the model is predicted and results are used for adaptation at the change-point. Moreover, the developed framework enables checking safety properties at runtime.
Maryam Bagheri, Ilge Akkaya, Ehsan Khamespanah, Narges Khakpour, Marjan Sirjani, Ali Movaghar, Edward A. Lee
Architecture-Based Design: A Satellite On-Board Software Case Study
Abstract
In this case study, we apply the architecture-based design approach to the control software of the CubETH satellite. Architectures are a means for ensuring global coordination properties and thus, achieving correctness of complex systems by construction. We illustrate the following three steps of the design approach: (1) definition of a domain-specific taxonomy of architecture styles; (2) design of the software model by applying architectures to enforce the required properties; (3) deadlock-freedom analysis of the resulting model. We provide a taxonomy of architecture styles for satellite on-board software, formally defined by architecture diagrams in the BIP component-based framework. We show how architectures are instantiated from the diagrams and applied to a set of atomic components. Deadlock-freedom of the resulting model is verified using DFinder from the BIP tool-set. We provide additional validation of our approach by using the nuXmv model checker to verify that the properties enforced by the architectures are, indeed, satisfied by the model.
Anastasia Mavridou, Emmanouela Stachtiari, Simon Bliudze, Anton Ivanov, Panagiotis Katsaros, Joseph Sifakis
Backmatter
Metadata
Title
Formal Aspects of Component Software
Editors
Olga Kouchnarenko
Ramtin Khosravi
Copyright Year
2017
Electronic ISBN
978-3-319-57666-4
Print ISBN
978-3-319-57665-7
DOI
https://doi.org/10.1007/978-3-319-57666-4

Premium Partner

    Image Credits