-
A Reference Architecture for Autonomous Networks: An Agent-Based Approach
Authors:
Joseph Sifakis,
Dongming Li,
Hairong Huang,
Yong Zhang,
Wenshuan Dang,
River Huang,
Yijun Yu
Abstract:
The vision of autonomous systems is becoming increasingly important in many application areas, where the aim is to replace humans with agents. These include autonomous vehicles and other agents' applications in business processes and problem-solving. For networks, the increasing scale and operation and management (O&M) complexity drive the need for autonomous networks (AN). The technical objective…
▽ More
The vision of autonomous systems is becoming increasingly important in many application areas, where the aim is to replace humans with agents. These include autonomous vehicles and other agents' applications in business processes and problem-solving. For networks, the increasing scale and operation and management (O&M) complexity drive the need for autonomous networks (AN). The technical objective of AN is to ensure trustworthy O&M without human intervention for higher efficiency and lower operating costs. However, realizing AN seems more difficult than autonomous vehicles. It encounters challenges of networks' structural and functional complexity, which operate as distributed dynamic systems governed by various technical and economic constraints. A key problem lies in formulating a rigorous development methodology that facilitates a seamless transition from traditional networks to AN. Central to this methodology is the definition of a reference architecture for network agents, which specifies the required functionalities for their realization, regardless of implementation choices. This article proposes a reference architecture characterizing main functional features, illustrating its application with network use cases. It shows how artificial intelligence components can be used to implement the required functionality and its coordination. The latter is achieved through the management and generation of shared domain-specific knowledge stored in long-term memory, ensuring the overall consistency of decisions and their execution. The article concludes with a discussion of architecture specialization for building network layer agents. It also identifies the main technical challenges ahead, such as satisfying essential requirements at development or runtime, as well as the issue of coordinating agents to achieve collective intelligence in meeting overall network goals.
△ Less
Submitted 18 March, 2025; v1 submitted 17 March, 2025;
originally announced March 2025.
-
A Comprehensive Evaluation of Four End-to-End AI Autopilots Using CCTest and the Carla Leaderboard
Authors:
Changwen Li,
Joseph Sifakis,
Rongjie Yan,
Jian Zhang
Abstract:
End-to-end AI autopilots for autonomous driving systems have emerged as a promising alternative to traditional modular autopilots, offering the potential to reduce development costs and mitigate defects arising from module composition. However, they suffer from the well-known problems of AI systems such as non-determinism, non-explainability, and anomalies. This naturally raises the question of th…
▽ More
End-to-end AI autopilots for autonomous driving systems have emerged as a promising alternative to traditional modular autopilots, offering the potential to reduce development costs and mitigate defects arising from module composition. However, they suffer from the well-known problems of AI systems such as non-determinism, non-explainability, and anomalies. This naturally raises the question of their evaluation and, in particular, their comparison with existing modular solutions.
This work extends a study of the critical configuration testing (CCTest) approach that has been applied to four open modular autopilots. This approach differs from others in that it generates test cases ensuring safe control policies are possible for the tested autopilots. This enables an accurate assessment of the ability to drive safely in critical situations, as any incident observed in the simulation involves the failure of a tested autopilot. The contribution of this paper is twofold.
Firstly, we apply the CCTest approach to four end-to-end open autopilots, InterFuser, MILE, Transfuser, and LMDrive, and compare their test results with those of the four modular open autopilots previously tested with the same approach implemented in the Carla simulation environment. This comparison identifies both differences and similarities in the failures of the two autopilot types in critical configurations.
Secondly, we compare the evaluations of the four autopilots carried out in the Carla Leaderboard with the CCTest results. This comparison reveals significant discrepancies, reflecting differences in test case generation criteria and risk assessment methods. It underlines the need to work towards the development of objective assessment methods combining qualitative and quantitative criteria.
△ Less
Submitted 24 March, 2025; v1 submitted 21 January, 2025;
originally announced January 2025.
-
World Models: The Safety Perspective
Authors:
Zifan Zeng,
Chongzhe Zhang,
Feng Liu,
Joseph Sifakis,
Qunli Zhang,
Shiming Liu,
Peng Wang
Abstract:
With the proliferation of the Large Language Model (LLM), the concept of World Models (WM) has recently attracted a great deal of attention in the AI research community, especially in the context of AI agents. It is arguably evolving into an essential foundation for building AI agent systems. A WM is intended to help the agent predict the future evolution of environmental states or help the agent…
▽ More
With the proliferation of the Large Language Model (LLM), the concept of World Models (WM) has recently attracted a great deal of attention in the AI research community, especially in the context of AI agents. It is arguably evolving into an essential foundation for building AI agent systems. A WM is intended to help the agent predict the future evolution of environmental states or help the agent fill in missing information so that it can plan its actions and behave safely. The safety property of WM plays a key role in their effective use in critical applications. In this work, we review and analyze the impacts of the current state-of-the-art in WM technology from the point of view of trustworthiness and safety based on a comprehensive survey and the fields of application envisaged. We provide an in-depth analysis of state-of-the-art WMs and derive technical research challenges and their impact in order to call on the research community to collaborate on improving the safety and trustworthiness of WM.
△ Less
Submitted 12 November, 2024;
originally announced November 2024.
-
Rigorous Simulation-based Testing for Autonomous Driving Systems -- Targeting the Achilles' Heel of Four Open Autopilots
Authors:
Changwen Li,
Joseph Sifakis,
Rongjie Yan,
Jian Zhang
Abstract:
Simulation-based testing remains the main approach for validating Autonomous Driving Systems. We propose a rigorous test method based on breaking down scenarios into simple ones, taking into account the fact that autopilots make decisions according to traffic rules whose application depends on local knowledge and context. This leads us to consider the autopilot as a dynamic system receiving three…
▽ More
Simulation-based testing remains the main approach for validating Autonomous Driving Systems. We propose a rigorous test method based on breaking down scenarios into simple ones, taking into account the fact that autopilots make decisions according to traffic rules whose application depends on local knowledge and context. This leads us to consider the autopilot as a dynamic system receiving three different types of vistas as input, each characterizing a specific driving operation and a corresponding control policy.
The test method for the considered vista types generates test cases for critical configurations that place the vehicle under test in critical situations characterized by the transition from cautious behavior to progression in order to clear an obstacle. The test cases thus generated are realistic, i.e., they determine the initial conditions from which safe control policies are possible, based on knowledge of the vehicle's dynamic characteristics. Constraint analysis identifies the most critical test cases, whose success implies the validity of less critical ones. Test coverage can therefore be greatly simplified. Critical test cases reveal major defects in Apollo, Autoware, and the Carla and LGSVL autopilots. Defects include accidents, software failures, and traffic rule violations that would be difficult to detect by random simulation, as the test cases lead to situations characterized by finely-tuned parameters of the vehicles involved, such as their relative position and speed.
Our results corroborate real-life observations and confirm that autonomous driving systems still have a long way to go before offering acceptable safety guarantees.
△ Less
Submitted 27 May, 2024;
originally announced May 2024.
-
Safe by Design Autonomous Driving Systems
Authors:
Marius Bozga,
Joseph Sifakis
Abstract:
Developing safe autonomous driving systems is a major scientific and technical challenge. Existing AI-based end-to-end solutions do not offer the necessary safety guarantees, while traditional systems engineering approaches are defeated by the complexity of the problem. Currently, there is an increasing interest in hybrid design solutions, integrating machine learning components, when necessary, w…
▽ More
Developing safe autonomous driving systems is a major scientific and technical challenge. Existing AI-based end-to-end solutions do not offer the necessary safety guarantees, while traditional systems engineering approaches are defeated by the complexity of the problem. Currently, there is an increasing interest in hybrid design solutions, integrating machine learning components, when necessary, while using model-based components for goal management and planning.
We study a method for building safe by design autonomous driving systems, based on the assumption that the capability to drive boils down to the coordinated execution of a given set of driving operations. The assumption is substantiated by a compositionality result considering that autopilots are dynamic systems receiving a small number of types of vistas as input, each vista defining a free space in its neighborhood. It is shown that safe driving for each type of vista in the corresponding free space, implies safe driving for any possible scenario under some easy-to-check conditions concerning the transition between vistas. The designed autopilot comprises distinct control policies one per type of vista, articulated in two consecutive phases. The first phase consists of carefully managing a potentially risky situation by virtually reducing speed, while the second phase consists of exiting the situation by accelerating.
The autopilots designed use for their predictions simple functions characterizing the acceleration and deceleration capabilities of the vehicles. They cover the main driving operations, including entering a main road, overtaking, crossing intersections protected by traffic lights or signals, and driving on freeways. The results presented reinforce the case for hybrid solutions that incorporate mathematically elegant and robust decision methods that are safe by design.
△ Less
Submitted 20 May, 2024;
originally announced May 2024.
-
Testing System Intelligence
Authors:
Joseph Sifakis
Abstract:
We discuss the adequacy of tests for intelligent systems and practical problems raised by their implementation. We propose the replacement test as the ability of a system to replace successfully another system performing a task in a given context. We show how it can characterize salient aspects of human intelligence that cannot be taken into account by the Turing test. We argue that building intel…
▽ More
We discuss the adequacy of tests for intelligent systems and practical problems raised by their implementation. We propose the replacement test as the ability of a system to replace successfully another system performing a task in a given context. We show how it can characterize salient aspects of human intelligence that cannot be taken into account by the Turing test. We argue that building intelligent systems passing the replacement test involves a series of technical problems that are outside the scope of current AI. We present a framework for implementing the proposed test and validating the properties of the intelligent systems. We discuss the inherent limitations of intelligent system validation and advocate new theoretical foundations for extending existing rigorous test methods. We suggest that the replacement test, based on the complementarity of skills between human and machine, can lead to a multitude of intelligence concepts reflecting the ability to combine data-based and symbolic knowledge to varying degrees.
△ Less
Submitted 12 August, 2023; v1 submitted 19 May, 2023;
originally announced May 2023.
-
Simulation-based Validation for Autonomous Driving Systems
Authors:
Changwen Li,
Joseph Sifakis,
Qiang Wang,
Rongjie Yan,
Jian Zhang
Abstract:
Simulation is essential to validate autonomous driving systems. However, a simple simulation, even for an extremely high number of simulated miles or hours, is not sufficient. We need well-founded criteria showing that simulation does indeed cover a large fraction of the relevant real-world situations. In addition, the validation must concern not only incidents, but also the detection of any type…
▽ More
Simulation is essential to validate autonomous driving systems. However, a simple simulation, even for an extremely high number of simulated miles or hours, is not sufficient. We need well-founded criteria showing that simulation does indeed cover a large fraction of the relevant real-world situations. In addition, the validation must concern not only incidents, but also the detection of any type of potentially dangerous situation, such as traffic violations.
We investigate a rigorous simulation and testing-based validation method for autonomous driving systems that integrates an existing industrial simulator and a formally defined testing environment. The environment includes a scenario generator that drives the simulation process and a monitor that checks at runtime the observed behavior of the system against a set of system properties to be validated. The validation method consists in extracting from the simulator a semantic model of the simulated system including a metric graph, which is a mathematical model of the environment in which the vehicles of the system evolve. The monitor can verify properties formalized in a first-order linear temporal logic and provide diagnostics explaining their non satisfaction. Instead of exploring the system behavior randomly as many simulators do, we propose a method to systematically generate sets of scenarios that cover potentially risky situations, especially for different types of junctions where specific traffic rules must be respected. We show that the systematic exploration of risky situations has uncovered many flaws in the real simulator that would have been very difficult to discover by a random exploration process.
△ Less
Submitted 21 January, 2023; v1 submitted 10 January, 2023;
originally announced January 2023.
-
Correct by Design Coordination of Autonomous Driving Systems
Authors:
Marius Bozga,
Joseph Sifakis
Abstract:
The paper proposes a method for the correct by design coordination of autonomous driving systems (ADS). It builds on previous results on collision avoidance policies and the modeling of ADS by combining descriptions of their static environment in the form of maps, and the dynamic behavior of their vehicles. An ADS is modeled as a dynamic system involving a set of vehicles coordinated by a Runtime…
▽ More
The paper proposes a method for the correct by design coordination of autonomous driving systems (ADS). It builds on previous results on collision avoidance policies and the modeling of ADS by combining descriptions of their static environment in the form of maps, and the dynamic behavior of their vehicles. An ADS is modeled as a dynamic system involving a set of vehicles coordinated by a Runtime that based on vehicle positions on a map and their kinetic attributes, computes free spaces for each vehicle. Vehicles are bounded to move within the corresponding allocated free spaces. We provide a correct by design safe control policy for an ADS if its vehicles and the Runtime respect corresponding assume-guarantee contracts. The result is established by showing that the composition of assume-guarantee contracts is an inductive invariant that entails ADS safety. We show that it is practically possible to define speed control policies for vehicles that comply with their contracts. Furthermore, we show that traffic rules can be specified in a linear-time temporal logic, as a class of formulas that constrain vehicle speeds. The main result is that, given a set of traffic rules, it is possible to derive free space policies of the Runtime such that the resulting system behavior is safe by design with respect to the rules.
△ Less
Submitted 20 May, 2022;
originally announced May 2022.
-
Verification of Component-based Systems with Recursive Architectures
Authors:
Marius Bozga,
Radu Iosif,
Joseph Sifakis
Abstract:
We study a sound verification method for parametric component-based systems. The method uses a resource logic, a new formal specification language for distributed systems consisting of a finite yet unbounded number of components. The logic allows the description of architecture configurations coordinating instances of a finite number of types of components, by means of inductive definitions simila…
▽ More
We study a sound verification method for parametric component-based systems. The method uses a resource logic, a new formal specification language for distributed systems consisting of a finite yet unbounded number of components. The logic allows the description of architecture configurations coordinating instances of a finite number of types of components, by means of inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. For parametric systems specified in this logic, we show that decision problems such as reaching deadlock or violating critical section are undecidable, in general. Despite this negative result, we provide for these decision problems practical semi-algorithms relying on the automatic synthesis of structural invariants allowing the proof of general safety properties. The invariants are defined using the WSkS fragment of the monadic second order logic, known to be decidable by a classical automata-logic connection, thus reducing a verification problem to checking satisfiability of a WSkS formula.
△ Less
Submitted 15 December, 2021;
originally announced December 2021.
-
Runtime Safety Assurance for Learning-enabled Control of Autonomous Driving Vehicles
Authors:
Shengduo Chen,
Yaowei Sun,
Dachuan Li,
Qiang Wang,
Qi Hao,
Joseph Sifakis
Abstract:
Providing safety guarantees for Autonomous Vehicle (AV) systems with machine-learning-based controllers remains a challenging issue. In this work, we propose Simplex-Drive, a framework that can achieve runtime safety assurance for machine-learning enabled controllers of AVs. The proposed Simplex-Drive consists of an unverified Deep Reinforcement Learning (DRL)-based advanced controller (AC) that a…
▽ More
Providing safety guarantees for Autonomous Vehicle (AV) systems with machine-learning-based controllers remains a challenging issue. In this work, we propose Simplex-Drive, a framework that can achieve runtime safety assurance for machine-learning enabled controllers of AVs. The proposed Simplex-Drive consists of an unverified Deep Reinforcement Learning (DRL)-based advanced controller (AC) that achieves desirable performance in complex scenarios, a Velocity-Obstacle (VO) based baseline safe controller (BC) with provably safety guarantees, and a verified mode management unit that monitors the operation status and switches the control authority between AC and BC based on safety-related conditions. We provide a formal correctness proof of Simplex-Drive and conduct a lane-changing case study in dense traffic scenarios. The simulation experiment results demonstrate that Simplex-Drive can always ensure operation safety without sacrificing control performance, even if the DRL policy may lead to deviations from the safe status.
△ Less
Submitted 27 September, 2021;
originally announced September 2021.
-
Specification and Validation of Autonomous Driving Systems: A Multilevel Semantic Framework
Authors:
Marius Bozga,
Joseph Sifakis
Abstract:
Autonomous Driving Systems (ADS) are critical dynamic reconfigurable agent systems whose specification and validation raises extremely challenging problems. The paper presents a multilevel semantic framework for the specification of ADS and discusses associated validation problems. The framework relies on a formal definition of maps modeling the physical environment in which vehicles evolve. Maps…
▽ More
Autonomous Driving Systems (ADS) are critical dynamic reconfigurable agent systems whose specification and validation raises extremely challenging problems. The paper presents a multilevel semantic framework for the specification of ADS and discusses associated validation problems. The framework relies on a formal definition of maps modeling the physical environment in which vehicles evolve. Maps are directed metric graphs whose nodes represent positions and edges represent segments of roads. We study basic properties of maps including their geometric consistency. Furthermore, we study position refinement and segment abstraction relations allowing multilevel representation from purely topological to detailed geometric. We progressively define first order logics for modeling families of maps and distributions of vehicles over maps. These are Configuration Logics, which in addition to the usual logical connectives are equipped with a coalescing operator to build configurations of models. We study their semantics and basic properties. We illustrate their use for the specification of traffic rules and scenarios characterizing sequences of scenes. We study various aspects of the validation problem including run-time verification and satisfiability of specifications. Finally, we show links of our framework with practical validation needs for ADS and advocate its adequacy for addressing the many facets of this challenge.
△ Less
Submitted 14 September, 2021;
originally announced September 2021.
-
A hybrid controller for safe and efficient collision avoidance control
Authors:
Qiang Wang,
Xinlei Zheng,
Jiyong Zhang,
Joseph Sifakis
Abstract:
We design and experimentally evaluate a hybrid safe-by-construction collision avoidance controller for autonomous vehicles. The controller combines into a single architecture the respective advantages of an adaptive controller and a discrete safe controller. The adaptive controller relies on model predictive control to achieve optimal efficiency in nominal conditions. The safe controller avoids co…
▽ More
We design and experimentally evaluate a hybrid safe-by-construction collision avoidance controller for autonomous vehicles. The controller combines into a single architecture the respective advantages of an adaptive controller and a discrete safe controller. The adaptive controller relies on model predictive control to achieve optimal efficiency in nominal conditions. The safe controller avoids collision by applying two different policies, for nominal and out-of-nominal conditions, respectively. We present design principles for both the adaptive and the safe controller and show how each one can contribute in the hybrid architecture to improve performance, road occupancy and passenger comfort while preserving safety. The experimental results confirm the feasibility of the approach and the practical relevance of hybrid controllers for safe and efficient driving.
△ Less
Submitted 29 March, 2021;
originally announced March 2021.
-
Safe and efficient collision avoidance control for autonomous vehicles
Authors:
Qiang Wang,
Dachuan Li,
Joseph Sifakis
Abstract:
We study a novel principle for safe and efficient collision avoidance that adopts a mathematically elegant and general framework abstracting as much as possible from the controlled vehicle's dynamics and of its environment. Vehicle dynamics is characterized by pre-computed functions for accelerating and braking to a given speed. Environment is modeled by a function of time giving the free distance…
▽ More
We study a novel principle for safe and efficient collision avoidance that adopts a mathematically elegant and general framework abstracting as much as possible from the controlled vehicle's dynamics and of its environment. Vehicle dynamics is characterized by pre-computed functions for accelerating and braking to a given speed. Environment is modeled by a function of time giving the free distance ahead of the controlled vehicle under the assumption that the obstacles are either fixed or are moving in the same direction. The main result is a control policy enforcing the vehicle's speed so as to avoid collision and efficiently use the free distance ahead, provided some initial safety condition holds. The studied principle is applied to the design of two discrete controllers, one synchronous and another asynchronous. We show that both controllers are safe by construction. Furthermore, we show that their efficiency strictly increases for decreasing granularity of discretization. We present implementations of the two controllers, their experimental evaluation in the Carla autonomous driving simulator and investigate various performance issues.
△ Less
Submitted 2 October, 2020; v1 submitted 10 August, 2020;
originally announced August 2020.
-
Structural Invariants for the Verification of Systems with Parameterized Architectures
Authors:
Marius Bozga,
Javier Esparza,
Radu Iosif,
Joseph Sifakis,
Christoph Welzel
Abstract:
We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components communicate by executing atomic interactions whose participants update their states simultaneously. We introduce an interaction logic to specify both the type of interactions (e.g.\ rendez-vous, broadcast) and the topology of…
▽ More
We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components communicate by executing atomic interactions whose participants update their states simultaneously. We introduce an interaction logic to specify both the type of interactions (e.g.\ rendez-vous, broadcast) and the topology of the system (e.g.\ pipeline, ring). The logic can be easily embedded in monadic second order logic of finitely many successors, and is therefore decidable.
Proving safety properties of such a parameterized system, like deadlock freedom or mutual exclusion, requires to infer an inductive invariant that contains all reachable states of all system instances, and no unsafe state. We present a method to automatically synthesize inductive invariants directly from the formula describing the interactions, without costly fixed point iterations. We experimentally prove that this invariant is strong enough to verify safety properties of a large number of systems including textbook examples (dining philosophers, synchronization schemes), classical mutual exclusion algorithms, cache-coherence protocols and self-stabilization algorithms, for an arbitrary number of components.
△ Less
Submitted 7 September, 2021; v1 submitted 18 February, 2020;
originally announced February 2020.
-
DesignBIP: A Design Studio for Modeling and Generating Systems with BIP
Authors:
Anastasia Mavridou,
Joseph Sifakis,
Janos Sztipanovits
Abstract:
The Behavior-Interaction-Priority (BIP) framework, rooted in rigorous semantics, allows the construction of systems that are correct-by-design. BIP has been effectively used for the construction and analysis of large systems such as robot controllers and satellite on-board software. Nevertheless, the specification of BIP models is done in a purely textual manner without any code editor support. To…
▽ More
The Behavior-Interaction-Priority (BIP) framework, rooted in rigorous semantics, allows the construction of systems that are correct-by-design. BIP has been effectively used for the construction and analysis of large systems such as robot controllers and satellite on-board software. Nevertheless, the specification of BIP models is done in a purely textual manner without any code editor support. To facilitate the specification of BIP models, we present DesignBIP, a web-based, collaborative, version-controlled design studio. To promote model scaling and reusability of BIP models, we use a graphical language for modeling parameterized BIP models with rigorous semantics. We present the various services provided by the design studio, including model editors, code editors, consistency checking mechanisms, code generators, and integration with the JavaBIP tool-set.
△ Less
Submitted 5 July, 2018;
originally announced November 2019.
-
Autonomics: In Search of a Foundation for Next Generation Autonomous Systems
Authors:
David Harel,
Assaf Marron,
Joseph Sifakis
Abstract:
The potential benefits of autonomous systems have been driving intensive development of such systems, and of supporting tools and methodologies. However, there are still major issues to be dealt with before such development becomes commonplace engineering practice, with accepted and trustworthy deliverables. We argue that a solid, evolving, publicly available, community-controlled foundation for d…
▽ More
The potential benefits of autonomous systems have been driving intensive development of such systems, and of supporting tools and methodologies. However, there are still major issues to be dealt with before such development becomes commonplace engineering practice, with accepted and trustworthy deliverables. We argue that a solid, evolving, publicly available, community-controlled foundation for developing next generation autonomous systems is a must. We discuss what is needed for such a foundation, identify a central aspect thereof, namely, decision-making, and focus on three main challenges: (i) how to specify autonomous system behavior and the associated decisions in the face of unpredictability of future events and conditions and the inadequacy of current languages for describing these; (ii) how to carry out faithful simulation and analysis of system behavior with respect to rich environments that include humans, physical artifacts, and other systems,; and (iii) how to engineer systems that combine executable model-driven techniques and data-driven machine learning techniques. We argue that autonomics, i.e., the study of unique challenges presented by next generation autonomous systems, and research towards resolving them, can introduce substantial contributions and innovations in system engineering and computer science.
△ Less
Submitted 16 November, 2019;
originally announced November 2019.
-
Local Reasoning about Parametric and Reconfigurable Component-based Systems
Authors:
Marius Bozga,
Radu Iosif,
Joseph Sifakis
Abstract:
We introduce a logical framework for the specification and verification of component-based systems, in which finitely many component instances are active, but the bound on their number is not known. Besides specifying and verifying parametric systems, we consider the aspect of dynamic reconfiguration, in which components can migrate at runtime on a physical map, whose shape and size may change. We…
▽ More
We introduce a logical framework for the specification and verification of component-based systems, in which finitely many component instances are active, but the bound on their number is not known. Besides specifying and verifying parametric systems, we consider the aspect of dynamic reconfiguration, in which components can migrate at runtime on a physical map, whose shape and size may change. We describe such parametric and reconfigurable architectures using resource logics, close in spirit to Separation Logic, used to reason about dynamic pointer structures. These logics support the principle of local reasoning, which is the key for writing modular specifications and building scalable verification algorithms, that deal with large industrial-size systems.
△ Less
Submitted 19 August, 2019;
originally announced August 2019.
-
Structural Invariants for Parametric Verification of Systems with Almost Linear Architectures
Authors:
Marius Bozga,
Radu Iosif,
Joseph Sifakis
Abstract:
We consider concurrent systems consisting of a finite but unknown number of components, that are replicated instances of a given set of finite state automata. The components communicate by executing interactions which are simultaneous atomic state changes of a set of components. We specify both the type of interactions (e.g.\ rendez-vous, broadcast) and the topology (i.e.\ architecture) of the sys…
▽ More
We consider concurrent systems consisting of a finite but unknown number of components, that are replicated instances of a given set of finite state automata. The components communicate by executing interactions which are simultaneous atomic state changes of a set of components. We specify both the type of interactions (e.g.\ rendez-vous, broadcast) and the topology (i.e.\ architecture) of the system (e.g.\ pipeline, ring) via a decidable interaction logic, which is embedded in the classical weak sequential calculus of one successor (WS1S). Proving correctness of such system for safety properties, such as deadlock freedom or mutual exclusion, requires the inference of an inductive invariant that subsumes the set of reachable states and avoids the unsafe states. Our method synthesizes such invariants directly from the formula describing the interactions, without costly fixed point iterations. We applied our technique to the verification of several textbook examples, such as dining philosophers, mutual exclusion protocols and concurrent systems with preemption and priorities.
△ Less
Submitted 7 February, 2019;
originally announced February 2019.
-
Checking Deadlock-Freedom of Parametric Component-Based Systems
Authors:
Marius Bozga,
Radu Iosif,
Joseph Sifakis
Abstract:
We propose an automated method for computing inductive invariants applied to check deadlock-freedom for parametric component-based systems. The method generalizes the approach for computing structural trap invariants from bounded to parametric systems with general architectures. It symbolically extracts trap invariants from a monadic interaction formula characterizing the system architecture. The…
▽ More
We propose an automated method for computing inductive invariants applied to check deadlock-freedom for parametric component-based systems. The method generalizes the approach for computing structural trap invariants from bounded to parametric systems with general architectures. It symbolically extracts trap invariants from a monadic interaction formula characterizing the system architecture. The paper presents the theoretical foundations of the method including new results for the first order monadic logic and proves its soundness. It also provides preliminary illustrations on examples.
△ Less
Submitted 15 February, 2019; v1 submitted 25 May, 2018;
originally announced May 2018.
-
DesignBIP: A Design Studio for Modeling and Generating Systems with BIP
Authors:
Anastasia Mavridou,
Joseph Sifakis,
Janos Sztipanovits
Abstract:
The Behavior-Interaction-Priority (BIP) framework, rooted in rigorous semantics, allows the construction of systems that are correct-by-design. BIP has been effectively used for the construction and analysis of large systems such as robot controllers and satellite on-board software. Nevertheless, the specification of BIP models is done in a purely textual manner without any code editor support. To…
▽ More
The Behavior-Interaction-Priority (BIP) framework, rooted in rigorous semantics, allows the construction of systems that are correct-by-design. BIP has been effectively used for the construction and analysis of large systems such as robot controllers and satellite on-board software. Nevertheless, the specification of BIP models is done in a purely textual manner without any code editor support. To facilitate the specification of BIP models, we present DesignBIP, a web-based, collaborative, version-controlled design studio. To promote model scaling and reusability of BIP models, we use a graphical language for modeling parameterized BIP models with rigorous semantics. We present the various services provided by the design studio, including model editors, code editors, consistency checking mechanisms, code generators, and integration with the JavaBIP tool-set.
△ Less
Submitted 31 May, 2018; v1 submitted 24 May, 2018;
originally announced May 2018.
-
DReAM: Dynamic Reconfigurable Architecture Modeling (full paper)
Authors:
Rocco De Nicola,
Alessandro Maggi,
Joseph Sifakis
Abstract:
Modern systems evolve in unpredictable environments and have to continuously adapt their behavior to changing conditions. The "DReAM" (Dynamic Reconfigurable Architecture Modeling) framework, has been designed for modeling reconfigurable dynamic systems. It provides a rule-based language, inspired from Interaction Logic, which is expressive and easy to use encompassing all aspects of dynamicity in…
▽ More
Modern systems evolve in unpredictable environments and have to continuously adapt their behavior to changing conditions. The "DReAM" (Dynamic Reconfigurable Architecture Modeling) framework, has been designed for modeling reconfigurable dynamic systems. It provides a rule-based language, inspired from Interaction Logic, which is expressive and easy to use encompassing all aspects of dynamicity including parametric multi-modal coordination with creation/deletion of components as well as mobility. Additionally, it allows the description of both endogenous/modular and exogenous/centralized coordination styles and sound transformations from one style to the other. The DReAM framework is implemented in the form of a Java API bundled with an execution engine. It allows to develop runnable systems combining the expressiveness of the rule-based notation together with the flexibility of this widespread programming language.
△ Less
Submitted 23 October, 2018; v1 submitted 9 May, 2018;
originally announced May 2018.
-
Architecture Diagrams: A Graphical Language for Architecture Style Specification
Authors:
Anastasia Mavridou,
Eduard Baranov,
Simon Bliudze,
Joseph Sifakis
Abstract:
Architecture styles characterise families of architectures sharing common characteristics. We have recently proposed configuration logics for architecture style specification. In this paper, we study a graphical notation to enhance readability and easiness of expression. We study simple architecture diagrams and a more expressive extension, interval architecture diagrams. For each type of diagrams…
▽ More
Architecture styles characterise families of architectures sharing common characteristics. We have recently proposed configuration logics for architecture style specification. In this paper, we study a graphical notation to enhance readability and easiness of expression. We study simple architecture diagrams and a more expressive extension, interval architecture diagrams. For each type of diagrams, we present its semantics, a set of necessary and sufficient consistency conditions and a method that allows to characterise compositionally the specified architectures. We provide several examples illustrating the application of the results. We also present a polynomial-time algorithm for checking that a given architecture conforms to the architecture style specified by a diagram.
△ Less
Submitted 10 August, 2016;
originally announced August 2016.
