This thesis provides a specification theory with strong algebraic and compositionality properties, allowing for the systematic construction of new components out of existing ones, while ensuring that given properties continue to hold at each stage of system development. The theory shares similarities with the interface automata of de Alfaro and Henzinger, but is linear-time in the style of Dill's trace theory, and is endowed with a richer collection of operators. Components are assumed to communicate with one another by synchronisation of input and output actions, with the component specifying the allowed sequences of interactions between itself and the environment. When the environment produces an interaction that the component is unwilling to receive, a communication mismatch occurs, which can correspond to run-time error or underspecification. These are modelled uniformly as inconsistencies. A linear-time refinement preorder corresponding to substitutivity preserves the absence of inconsistency under all environments, allowing for the safe replacement of components at run-time. To build complex systems, a range of compositional operators are introduced, including parallel composition, logical conjunction and disjunction, hiding, and quotient. These can be used to examine the structural behaviour of a system, combine independently developed requirements, abstract behaviour, and incrementally synthesise missing components, respectively. It is shown that parallel composition is monotonic under refinement, conjunction and disjunction correspond to the meet and join operations on the refinement preorder, and quotient is the adjoint of parallel composition. Full abstraction results are presented for the equivalence defined as mutual refinement, a consequence of the refinement being the weakest preorder capturing substitutivity. Extensions of the specification theory with progress-sensitivity (ensuring that refinement cannot introduce quiescence) and real-time constraints on when interactions may and may not occur are also presented. These theories are further complemented by assume-guarantee frameworks for supporting component-based reasoning, where contracts (characterising sets of components) separate the assumptions placed on the environment from the guarantees provided by the components. By defining the compositional operators directly on contracts, sound and complete assume-guarantee rules are formulated that preserve both safety and progress. Examples drawn from distributed systems are used to demonstrate how these rules can be used for mechanically deriving component-based designs.

Safety-critical systems have garnered increasing attention, particularly regarding their dependability analysis. In modern times, these systems comprise numerous components, making it crucial to verify that lower-level components adhere to their specifications will ensure the overall system’s compliance with its top-level specification. However, two issues arise in this verification process. Firstly, many industrial applications lack lower-level natural-language specifications for their components, relying solely on toplevel specifications. Secondly, many current verification algorithms need to explore the continuous time evolution of the behavioral combinations of these components, and the combination of components to be explored will rise exponentially with the number of components. To address these challenges, this paper presents significant contributions. Firstly, it introduces a novel method that leverages the structures of redundancy systems to create naturallanguage specifications for components derived from a top-level specification. This approach facilitates a more efficient decomposition of the top-level specification, allowing for greater ease in handling component behaviors. Secondly, the proposed method is successfully applied to Scania’s brake system, leading to the decomposition of its top-level specification. To verify this decomposition, an existing verification algorithm is selected, and the results are impressive. The proposed method effectively addresses the issue of exponential growth in component behavior combinations, which was previously mentioned. Specifically, in the case of the Scania brake system, the number of combinations is dramatically reduced from 27 to a mere 13, showcasing the significant improvement achieved with the new method. / Säkerhetskritiska system har fått ökad uppmärksamhet, särskilt när det gäller deras pålitlighetsanalys. I moderna tider består dessa system av talrika komponenter, vilket gör det avgörande att verifiera att komponenter på lägre nivå följer sina specifikationer för att säkerställa att hela systemet följer sin övergripande specifikation. Två utmaningar uppstår dock i denna verifieringsprocess. För det första saknar många industriella tillämpningar naturligspråksspecifikationer för komponenter på lägre nivå och förlitar sig enbart på övergripande specifikationer. För det andra behöver många nuvarande verifieringsalgoritmer utforska de kontinuerliga tidsutvecklingarna av beteendekombinationer hos dessa komponenter, och antalet kombinationer som ska utforskas ökar exponentiellt med antalet komponenter. För att tackla dessa utmaningar presenterar den här artikeln betydande bidrag. För det första introducerar den en ny metod som utnyttjar strukturer i redundanta system för att skapa naturligspråksspecifikationer för komponenter som härleds från en övergripande specifikation. Denna metod underlättar en mer effektiv uppdelning av övergripande specifikation, vilket gör det enklare att hantera komponentbeteenden. För det andra tillämpas den föreslagna metoden framgångsrikt på Scanias bromssystem, vilket leder till en uppdelning av dess övergripande specifikation. För att verifiera denna uppdelning väljs en befintlig verifieringsalgoritm, och resultaten är imponerande. Den föreslagna metoden hanterar effektivt problemet med exponentiell tillväxt i komponentbeteendekombinationer, vilket tidigare nämnts. Specifikt, för Scanias bromssystem minskar antalet kombinationer dramatiskt från 27 till endast 13, vilket tydligt visar den betydande förbättring som uppnåtts med den nya metoden.

Les programmes informatiques prennent une place de plus en plus importante dans nos vies. Certains de ces programmes, comme par exemple les systèmes de contrôle de centrales électriques, d'avions ou de systèmes médicaux sont critiques : une panne ou un dysfonctionnement pourraient causer la perte de vies humaines ou des dommages matériels ou environnementaux importants. Les méthodes formelles visent à offrir des moyens de concevoir et vérifier de tels systèmes afin de garantir qu'ils fonctionneront comme prévu. Au fil du temps, ces systèmes deviennent de plus en plus évolués et complexes, ce qui est source de nouveaux défis pour leur vérification. Il devient nécessaire de développer ces systèmes de manière modulaire afin de pouvoir distribuer la tâche d'implémentation à différentes équipes d'ingénieurs. De plus, il est important de pouvoir réutiliser des éléments certifiés et les adapter pour répondre à de nouveaux besoins. Aussi les méthodes formelles doivent évoluer afin de s'adapter à la conception et à la vérification de ces systèmes modulaires de taille toujours croissante. Nous travaillons sur une approche algébrique pour la conception de systèmes corrects par construction. Elle définit un formalisme pour exprimer des spécifications de haut niveau et permet de les raffiner de manière incrémentale en des spécifications plus concrètes tout en préservant leurs propriétés, jusqu'à ce qu'une implémentation soit atteinte. Elle définit également plusieurs opérations permettant de construire des systèmes complexes à partir de composants plus simples en fusionnant différents points de vue d'un même système ou en composant plusieurs sous-systèmes ensemble, ainsi que de décomposer une spécification complexe afin de réutiliser des composants existants et de simplifier la tâche d'implémentation. Le formalisme de spécification que nous utilisons est basé sur des spécifications modales. Intuitivement, une spécification modale est un automate doté de deux types de transitions permettant d'exprimer des comportements optionnels ou obligatoires. Raffiner une spécification modale revient à décider si les parties optionnelles devraient être supprimées ou rendues obligatoires. Cette thèse contient deux principales contributions théoriques basées sur une extension des spécifications modales appelée " spécifications à ensembles d'acceptation ". La première contribution est l'identification d'une sous-classe des spécifications à ensembles d'acceptation, appelée " spécifications à ensembles d'acceptation convexes ", qui permet de définir des opérations bien plus efficaces tout en gardant un haut niveau d'expressivité. La seconde contribution est la définition d'un nouveau formalisme, appelé " spécifications à ensembles d'acceptation marquées ", qui permet d'exprimer des propriétés d'atteignabilité. Ceci peut, par exemple, être utilisé pour s'assurer qu'un système termine ou exprimer une propriété de vivacité dans un système réactif. Les opérations usuelles sont définies sur ce nouveau formalisme et elles garantissent la préservation des propriétés d'atteignabilité. Cette thèse présente également des résultats d'ordre plus pratique. Tous les résultats théoriques sur les spécifications à ensembles d'acceptation convexes ont été prouvés en utilisant l'assistant de preuves Coq. L'outil MAccS a été développé pour implémenter les formalismes et opérations présentés dans cette thèse. Il permet de les tester aisément sur des exemples, ainsi que d'étudier leur efficacité sur des cas concrets. / Software programs are taking a more and more important place in our lives. Some of these programs, like the control systems of power plants, aircraft, or medical devices for instance, are critical: a failure or malfunction could cause loss of human lives, damages to equipments, or environmental harm. Formal methods aim at offering means to design and verify such systems in order to guarantee that they will work as expected. As time passes, these systems grow in scope and size, yielding new challenges. It becomes necessary to develop these systems in a modular fashion to be able to distribute the implementation task to engineering teams. Moreover, being able to reuse some trustworthy parts of the systems and extend them to answer new needs in functionalities is increasingly required. As a consequence, formal methods also have to evolve in order to accommodate both the design and the verification of these larger, modular systems and thus address their scalability challenge. We promote an algebraic approach for the design of correct-by-construction systems. It defines a formalism to express high-level specifications of systems and allows to incrementally refine these specifications into more concrete ones while preserving their properties, until an implementation is reached. It also defines several operations allowing to assemble complex systems from simpler components, by merging several viewpoints of a specific system or composing several subsystems together, as well as decomposing a complex specification in order to reuse existing components and ease the implementation task. The specification formalism we use is based on modal specifications. In essence, a modal specification is an automaton with two kinds of transitions allowing to express mandatory and optional behaviors. Refining a modal specification amounts to deciding whether some optional parts should be removed or made mandatory. This thesis contains two main theoretical contributions, based on an extension of modal specifications called acceptance specifications. The first contribution is the identification of a subclass of acceptance specifications, called convex acceptance specifications, which allows to define much more efficient operations while maintaining a high level of expressiveness. The second contribution is the definition of a new formalism, called marked acceptance specifications, that allows to express some reachability properties. This could be used for example to ensure that a system is terminating or to express a liveness property for a reactive system. Usual operations are defined on this new formalism and guarantee the preservation of the reachability properties as well as independent implementability. This thesis also describes some more practical results. All the theoretical results on convex acceptance specifications have been proved using the Coq proof assistant. The tool MAccS has been developed to implement the formalisms and operations presented in this thesis. It allows to test them easily on some examples, as well as run some experimentations and benchmarks.