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

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben

2021 | Buch

Learning Assumptions for Verifying Cryptographic Protocols Compositionally Kapitel lesen Erstes Kapitel lesen

Formal Aspects of Component Software

17th International Conference, FACS 2021, Virtual Event, October 28–29, 2021, Proceedings

herausgegeben von: Gwen Salaün, Dr. Anton Wijs

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
insite
SUCHEN

Über dieses Buch

This book constitutes the thoroughly revised selected papers from the 17th International Symposium, FACS 2021, which was hel virtually in October 2021.
The 7 full papers and 1 short contribution were carefully reviewed and selected from 16 submissions and are presented in the volume together with 1 invited paper. FACS 2021 is concerned with how formal methods can be applied to component-based software and system development. The book is subdivided into two blocks: Modelling & Composition and Verification. Chapter "A Linear Parallel Algorithm to Compute Bisimulation and Relational Coarsest Partitions" is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com.

Inhaltsverzeichnis

Frontmatter

Invited Paper

Frontmatter
Learning Assumptions for Verifying Cryptographic Protocols Compositionally
Abstract
Automated analysis tools for cryptographic protocols can verify sophisticated designs, but lack compositionality. To address this limitation, we investigate the use of automata learning for verifying authentication protocols in an automatic and compositional way. We present Taglierino, a tool for synthesizing specifications for protocol components and checking them in isolation. The specifications can aid the design of protocol variants and speed up verification. Taglierino includes a domain-specific language for protocols, which are compiled to automata and analyzed with the LTSA model checker extended with automata learning. We demonstrate the tool on a series of case studies, including the Needham-Schroeder, Woo-Lam, and Kerberos protocols.
Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, Corina Păsăreanu

Modelling and Composition

Frontmatter
Component-Based Approach Combining UML and BIP for Rigorous System Design
Abstract
The development of critical systems requires the definition of a rigorous design approach enabling to check these systems before a real operation. This paper presents a component-based approach that combines UML and BIP languages for the specification and formal verification of systems. We begin by modeling the system architecture and behavior using UML. The UML models are then translated into a formal specification expressed in BIP. Finally, the SBIP framework is used for verifying the correctness of the system using Statistical Model Checking while satisfying requirements expressed by temporal properties. We apply our approach to a dam infrastructure, represented by a set of deployed sensors.
Salim Chehida, Abdelhakim Baouya, Saddek Bensalem
Composable Partial Multiparty Session Types
Abstract
We introduce partial sessions and partial (multiparty) session types, in order to deal with open systems, i.e., systems with missing components. Partial sessions can be composed, and the type of the resulting system is derived from those of its components without knowing any suitable global type nor the types of missing parts. Incompatible types, due to e.g. miscommunications or deadlocks, are detected at the merging phase. We apply these types to a process calculus, for which we prove subject reduction and progress, so that well-typed systems never violate the prescribed constraints. Therefore, partial session types support the development of systems by incremental assembling of components.
Claude Stolze, Marino Miculan, Pietro Di Gianantonio
A Canonical Algebra of Open Transition Systems
Abstract
Feedback and state are closely interrelated concepts. Categories with feedback, originally proposed by Katis, Sabadini and Walters, are a weakening of the notion of traced monoidal categories, with several pertinent applications in computer science. The construction of the free such categories has appeared in several different contexts, and can be considered as state bootstrapping. We show that a categorical algebra for open transition systems, \(\mathbf {Span}(\mathbf {Graph})_*\), also due to Katis, Sabadini and Walters, is the free category with feedback over \(\mathbf {Span}(\mathbf {Set})\). This algebra of transition systems is obtained by adding state to an algebra of predicates, and therefore \(\mathbf {Span}(\mathbf {Graph})_*\) is the canonical such algebra.
Elena Di Lavore, Alessandro Gianola, Mario Román, Nicoletta Sabadini, Paweł Sobociński
Corinne, a Tool for Choreography Automata
Abstract
Choreography automata are a model of choreographies envisaging high-level views of the behaviour of communicating systems as finite-state automata. The behaviour of each participant of a choreography can be obtained via a projection operation from a choreography automaton. The system of participants obtained by projection is well-behaved if the choreography automaton satisfies some well-formedness conditions. We present Corinne, a tool allowing one to render, compute projections of and compose choreography automata, as well as to check well-formedness conditions.
Simone Orlando, Vairo Di Pasquale, Franco Barbanera, Ivan Lanese, Emilio Tuosto

Verification

Frontmatter
Specification and Safety Verification of Parametric Hierarchical Distributed Systems
Abstract
We introduce a term algebra as a new formal specification language for the coordinating architectures of distributed systems consisting of a finite yet unbounded number of components. The language allows to describe infinite sets of systems whose coordination between components share the same pattern, using inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. Further, we give a verification method for the parametric systems described in this language, relying on the automatic synthesis of structural invariants that enable proving general safety properties (absence of deadlocks and critical section violations). The invariants are defined using the \(\mathsf {WS}{\kappa }\mathsf {S}\) fragment of the monadic second order logic, known to be decidable by a classical automata-logic connection. This reduces the safety verification problem to checking satisfiability of a \(\mathsf {WS}{\kappa }\mathsf {S}\) formula. We implemented the invariant synthesis method into a prototype tool and carried out verification experiments on a number of non-trivial models specified using the term algebra.
Marius Bozga, Radu Iosif

Open Access

A Linear Parallel Algorithm to Compute Bisimulation and Relational Coarsest Partitions
Abstract
The most efficient way to calculate strong bisimilarity is by finding the relational coarsest partition of a transition system. We provide the first linear-time algorithm to calculate strong bisimulation using parallel random access machines (PRAMs). More precisely, with n states, m transitions and \(| Act |\le m\) action labels, we provide an algorithm for \(\max (n,m)\) processors that calculates strong bisimulation in time \(\mathcal {O}(n+| Act |)\) and space \(\mathcal {O}(n+m)\). The best-known PRAM algorithm has time complexity \(\mathcal {O}(n\log n)\) on a smaller number of processors making it less suitable for massive parallel devices such as GPUs. An implementation on a GPU shows that the linear time-bound is achievable on contemporary hardware.
Jan Martens, Jan Friso Groote, Lars van den Haak, Pieter Hijma, Anton Wijs
PDF Zum Volltext
Automated Generation of Initial Configurations for Testing Component Systems
Abstract
In the context of component-based systems, this paper presents the automated generation of initial states, from which an adaptive system starts to receive sequences of events that aim to provoke reconfigurations. For generating these states, also called configurations, we present a combinatorial algorithm supporting various architectural elements and relationships among them, while satisfying consistency constraints expressed by invariants. Moreover, this algorithm deals with the system-dependant instantiations of the primitive and composite components, parameters and relations, in order to produce meaningful structured configurations. While testing adaptation policies for component-based systems, this algorithm allows us to improve the capability of fulfilling coverage criteria by using different initial configurations. To illustrate the approach, the paper reports on experiments on a simulation with platoons of autonomous vehicles.
Frédéric Dadeau, Jean-Philippe Gros, Olga Kouchnarenko
Monitoring Distributed Component-Based Systems
Abstract
We monitor asynchronous distributed component-based systems with multi-party interactions. We consider independent components whose interactions are managed by several distributed schedulers. In this context, neither a global state nor the total ordering of the executions of the system is available at runtime. We instrument the system to retrieve local events from the local traces of the schedulers. Local events are sent to a global observer which reconstructs on-the-fly the set of global traces that are compatible with the local traces, in a concurrency-preserving fashion. The set of compatible global traces is represented in the form of an original lattice over partial states, such that each path of the lattice corresponds to a possible execution of the system.
Yliès Falcone, Hosein Nazarpour, Saddek Bensalem, Marius Bozga
Backmatter
Metadaten
Titel
Formal Aspects of Component Software
herausgegeben von
Gwen Salaün
Dr. Anton Wijs
Copyright-Jahr
2021
Electronic ISBN
978-3-030-90636-8
Print ISBN
978-3-030-90635-1
DOI
https://doi.org/10.1007/978-3-030-90636-8

Premium Partner

    Bildnachweise