arXiv subjects

Joseph Sifakis

Publications and source records attributed to Joseph Sifakis.

29 records · Page 2Linked to original sources

arXiv2020

Safe and efficient collision avoidance control for autonomous vehicles

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.

eess.SY↗

arXiv2019

Autonomics: In Search of a Foundation for Next Generation Autonomous Systems

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.

cs.SE↗

arXiv2019

Local Reasoning about Parametric and Reconfigurable Component-based Systems

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.

cs.LO↗

arXiv2019

Checking Deadlock-Freedom of Parametric Component-Based Systems

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.

cs.LO↗

arXiv2019

Structural Invariants for Parametric Verification of Systems with Almost Linear Architectures

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.

cs.FL↗

arXiv2018

Autonomous Systems -- An Architectural Characterization

The concept of autonomy is key to the IoT vision promising increasing integration of smart services and systems minimizing human intervention. This vision challenges our capability to build complex open trustworthy autonomous systems. We lack a rigorous common semantic framework for autonomous systems. It is remarkable that the debate about autonomous vehicles focuses almost exclusively on AI and learning techniques while it ignores many other equally important autonomous system design issues. Autonomous systems involve agents and objects coordinated in some common environment so that their collective behavior meets a set of global goals. We propose a general computational model combining a system architecture model and an agent model. The architecture model allows expression of dynamic reconfigurable multi-mode coordination between components. The agent model consists of five interacting modules implementing each one a characteristic function: Perception, Reflection, Goal management, Planning and Self-adaptation. It determines a concept of autonomic complexity accounting for the specific difficulty to build autonomous systems. We emphasize that the main characteristic of autonomous systems is their ability to handle knowledge and adaptively respond to environment changes. We advocate that autonomy should be associated with functionality and not with specific techniques. Machine learning is essential for autonomy although it can meet only a small portion of the needs implied by autonomous system design. We conclude that autonomy is a kind of broad intelligence. Building trustworthy and optimal autonomous systems goes far beyond the AI challenge.

eess.SY↗

arXiv2018

DReAM: Dynamic Reconfigurable Architecture Modeling (full paper)

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.

cs.FL↗

arXiv2018

DesignBIP: A Design Studio for Modeling and Generating Systems with BIP

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.

cs.SE↗

arXiv2018

System Design in the Era of IoT --- Meeting the Autonomy Challenge

The advent of IoT is a great opportunity to reinvigorate Computing by focusing on autonomous system design. This certainly raises technology questions but, more importantly, it requires building new foundation that will systematically integrate the innovative results needed to face increasing environment and mission complexity. A key idea is to compensate the lack of human intervention by adaptive control. This is instrumental for system resilience: it allows both coping with uncertainty and managing mixed criticality services. Our proposal for knowledge-based design seeks a compromise: preserving rigorousness despite the fact that essential properties cannot be guaranteed at design time. It makes knowledge generation and application a primary concern and aims to fully and seamlessly incorporate the adaptive control paradigm in system architecture.

eess.SY↗

arXiv2018

DesignBIP: A Design Studio for Modeling and Generating Systems with BIP

cs.SE↗

arXiv2016

Architecture Diagrams: A Graphical Language for Architecture Style Specification

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.

cs.SE↗