The International Symposium on Formal Aspects of Component Software (FACS) was inaugurated two decades ago in response to the major software development paradigm shift from structured development and object-oriented development to component-based software development (CBSD) and service-oriented architecture (SOA). FACS is dedicated to fostering a deeper understanding of the distinctive aspects, promoting research, education, technological advancement, and the practical application of CBSD technology. On the 20th anniversary of FACS, it is appropriate to briefly recall its background and history, thereby highlighting its contributions to the community. Taking this opportunity, we focus on the discussion to elucidate the important aspects of component software that require to be and have been considered in formal theories. Leveraging the refinement of component and object-oriented systems (rCOS) as a framework, we provide an overview of these formal theories and discuss their relationships. We intend to express a vision that different theories and methods are required for different aspects in a CBSD process, and also different formal theories are required even for a particular aspect. However, ensuring their consistent application remains a major challenge and this is a main barrier to the effective industry adoption of CBSD. Furthermore, we delineate emerging challenges and prospects associated with integrating formal methods for modelling and design human-cyber-physical systems (HCPS) - hybrid integration encompassing cyber systems, physical systems, and the mixed human and machine intelligence.
Reactive graphs are transition structures whereas edges become active and inactive during its evolution, that were introduced by Dov Gabbay from a mathematical’s perspective. This paper presents ( https://fm-dcc.github.io/MARGe ), a web-based tool to visualise and analyse reactive graphs enriched with labels. animates the operational semantics of reactive graphs and offers different graphical views to provide insights over concrete systems. We motivate the applicability of reactive graphs for adaptive systems and for featured transition systems, using to tighten the gap between the existing theoretical models and their usage to analyse concrete systems.
Developers tend to be reluctant to provide formal specifications for software components; even well-established design-by-contract (DbC) properties like invariants, pre- and postconditions are neglected. This has hindered a more widely practical dissemination of the DbC paradigm. In this paper, we employ state-of-the-art NL processing technologies, using Large Language Models (LLMs), particularly, ChatGPT, to automatically infer formal specifications from component textual behavioural descriptions. More specifically, we implemented a framework (DbC-GPT), parameterised by a context, which is able to generate postcondition specifications for smart contract functions implemented in Solidity. The output of DbC-GPT is in the notation of the solc-verify tool (a verifier for Solidity) that is used to: (i) check the syntax of the inferred specification; and (ii) verify whether a reference implementation conforms to this specification. This is carried out in a loop in such a way that the DbC-GPT context is iteratively improved with verification counterexamples. To evaluate DbC-GPT, we have used some Ethereum standards (ERC20, ERC721, and ERC1155) and compared the precision of the generated specifications for several GPT contexts that consider information of these standards in isolation as well as their combination.
This paper focuses on the preliminary steps of developing safety-critical systems. We investigate how patterns could be used to generate Event-B refinements automatically. The patterns proposed in this paper either impose constraints on the model through weakest precondition calculus, superpose counters, or introduce de-synchronization mechanisms using observers. We show how the weakest precondition calculus integrated into the patterns can be simplified and become usable. Moreover, for our patterns to be fully usable in subsequent refinement steps, we produce as much as possible readable Event-B models. Finally, we revisit a classic case study using our proposed patterns.
Information flow security is not guaranteed to be preserved when a system is being composed of secure components. Whereas asynchronous communication is known to mitigate this problem in principle, the concrete impact of specific communication models on composability has not been investigated so far. We address this problem by formalizing seven asynchronous communication models from the literature in the Uppaal environment. On this basis, we capture a negative example, where information flow security is not composable, and contrast it with the formalized communication models to investigate their impact on composability. Our investigation shows that six out of seven asynchronous communication models ensure composability of information flow security.
A formal verification method for behavior tree (BT) is proposed. The method is based on a compositional model transformation of BT into the formal component-based system design framework BIP (Behavior-Interaction-Priority). The transformation encodes each BT node as an individual BIP component that is formally defined by an extended finite state automaton (FSA), and each BT edge as a set of interactions that describes the allowed coordination between components. The correctness proof of the model transformation is presented, and a prototype tool-chain has been implemented that enables the automated verification of BT. Two practical case studies show that the tool-chain can not only verify the correctness of BT, but also detect the potential design flaws automatically.
Fault handling is the timely and crash-free response to critical changes in a system's operating characteristics, such as rapid temperature increases, or electrical shorts. In a typical computer system, it is the board management controller's job to correctly respond to such anomalous situations. We develop an Isabelle/HOL model of a state machine for fault handling and define semantics for correctness of this procedure. Additionally, we formalize a notion of refinement that allows us to prove the correctness of implementations of this state machine. We also provide the first verified implementation of a C-based fault handler for board management controllers. Our implementation and the accompanying proofs are open-sourced and available online. Furthermore, we successfully deploy our verified fault handler on top of the seL4 microkernel and alongside a production-grade, open source software stack widely deployed today, applying the cyber-retrofit approach to securing board management controllers in practice. The implementation and proof effort required is moderate, and our efforts indicate that already a small team of a handful of people can significantly raise the level of assurance of a modern, highly privileged software system.
Rotation matrices, Euler angles, axis-angle, and unit quaternions are common models for representing object pose in space. Each offers distinct advantages and disadvantages regarding handling singularities, computational complexity, and storage requirements, motivating their interchangeability and conversion algorithms. However, these models and their associated algorithms involve complex matrix operations, trigonometric computations, and geometric reasoning, making manual derivation and verification error-prone. To guarantee algorithm correctness, we present a formal verification of these models and their conversion algorithms within the Coq Proof Assistant, focusing on pure rotational orientation representation. We establish a formal foundational mathematical library, including vector and matrix theories on abstract elements, additional real matrix properties, and quaternion theory. Building upon this foundation, we formalize all four rotation models and their conversion algorithms, emphasizing invariants of special orthogonal groups, Rodrigues' rotation formula, and the quaternion rotation formula. Our formally verified library offers excellent readability, usability, and simplicity, laying a foundation for developers to understand and verify advanced kinematics algorithms.
The reliability of concurrent and distributed systems often depends on some well-known techniques for fault tolerance. One such technique is based on checkpointing and rollback recovery. Checkpointing involves processes to take snapshots of their current states regularly, so that a rollback recovery strategy is able to bring the system back to a previous consistent state whenever a failure occurs. In this paper, we consider a message-passing concurrent programming language and propose a novel rollback recovery strategy that is based on some explicit checkpointing operators and the use of a (partially) reversible semantics for rolling back the system.
Compositionality supports the manipulation of large systems by working on their components. For model-based testing, this means that large systems can be tested by modelling and testing their components: passing tests for all components implies passing tests for the whole system. In previous work [14], we defined mutual acceptance for specification models and proved that this is a sufficient condition for compositionality in model-based testing. In this paper, we present an algorithm for verifying mutual acceptance on specifications and a sound and exhaustive model-based test procedure for checking mutual acceptance on black-box implementations, both inspired by the idea of environmental conformance [8, 9]. The result is that correctness of large systems can be determined by testing the component implementations for conformance to their component specification and for environmental conformance to the specification of their environment.
Many visions for model-driven component-based development emphasize models as the “single source of truth” by which different forms of analysis, specification, verification, and code generation are integrated. Such a vision depends strongly on a clear modeling language semantics that provides different tools and stakeholders with a common understanding of a model’s meaning. In this paper, we report on a mechanization of a formal semantics in the Isabelle theorem prover for key aspects of the SAE standard AADL modeling language. A primary goal of this semantics is to support component-oriented contract specification and verification as well as code generation implemented in the HAMR AADL model-driven development tool chain. We provide formal definitions of run-time system state, execution steps, reachable states, and property verification. Use of the mechanization for real-world applications is supported by automated HAMR translation from AADL models into the Isabelle specifications. In addition to general verification support, we define well-formedness properties and associated proofs for models, system states, and traces that are automatically proven for HAMR-generated Isabelle models.
This paper provides an overview on recent work on Team Automata, whereby a network of automata interacts by synchronising actions from multiple senders and receivers. We further revisit this notion of synchronisation in other well known concurrency models, such as Reo, BIP, Choreography Automata, and Multiparty Session Types. We address realisability of Team Automata, i.e., how to infer a network of interacting automata from a global specification, taking into account that this realisation should satisfy exactly the same properties as the global specification. In this analysis we propose a set of interesting directions of challenges and future work in the context of Team Automata or similar concurrency models.
Modeling and verifying the behavior of Cyber-Physical Systems (CPS) with complex interactions is challenging. Traditional languages such as SysML diagrams are not enough to capture CPS coordination. In this paper, we propose a novel approach called SysReo, which extends SysML diagrams (RD, BDD, IBD, SD) with the Reo coordination language. Our main objective is to enhance the interoperability of CPS by providing a more precise representation of system behavior and interaction protocols. To achieve this goal, we extend the SysML sequence diagram (SD) with Reo to create the SysReo SD. Through this integration, we bridge the gap between traditional modeling languages and the coordination demands of CPS. We develop an algorithm to generate Constraint Automata (CA) from SysReo SD, which ensures that CPS components can seamlessly work together. These automata are used in a verification tool that checks formulas expressed in Linear Temporal Logic (LTL). By leveraging LTL and Constraint Automata, we enhance the precision and rigor of CPS verification processes, while guaranteeing that CPS components can seamlessly work together. Furthermore, we apply our approach to a medical CPS case study, illustrating its effectiveness in identifying design flaws early and ensuring system behavior aligns with desired properties.
Component-based software engineering (CBSE) is a widely used software development paradigm. With software systems becoming increasingly sophisticated, CBSE provides an effective approach to construct reusable, extensible, and maintainable software systems. Formal verification provides a rigorous and systematic approach to validate the correctness of software systems by mathematically proving properties or checking them exhaustively against specified requirements. Using formal verification techniques in component-based development can further enhance the correctness of the development process. However, the adoption of component-based development supported by formal methods is hardly widespread in the industry. It serves to a limited extent in domains with stringent requirements for safety and reliability. In this paper, we aim to analyze the successful application scenarios of formal methods in component-based development, identify the challenges faced during their application, and explore methods to further broaden their adoption.
A promising way of integrating formal methods into industrial system design is to endow industrial modeling tools with automatic formal analyses. In this paper we identify some challenges for providing such formal methods “backends” for cyber-physical systems (CPSs), and argue that Maude could meet these challenges. We then give an overview of our research on integrating Maude analysis into the OSATE tool environment for the industrial CPS modeling standard AADL. Since many critical distributed CPSs are “logically synchronous,” a key feature making automatic formal analysis practical is the use of synchronizers for CPSs. We identify a sublanguage of AADL to describe synchronous CPS designs. We can then use Maude to effectively verify such synchronous designs, which under certain conditions also verifies the corresponding asynchronous distributed systems, with clock skews and communication delays. We then explain how we have extended our methods to multirate systems and to CPSs with continuous behaviors. We illustrate the effectiveness of Maude-based formal model engineering of industrial CPSs on avionics control systems and collections of drones. Finally, we identify future directions in this line of research.
Deciding how data should be transferred among Web services is an important part of their architecture design. Basically, each piece of data is transferred in either PUSH or PULL style. The architect’s selection of data transfer methods generally has a great impact on both the overall structure and performance of Web services. However, little work has been done on helping architects to select suitable data transfer methods. In this paper, we present a formal model to abstract some parts of Web services architecture that are not affected by the selection of data transfer methods, and based on the model, we propose an architecture level refactoring for changing data transfer methods. Also, we present an algorithm to generate prototypes of Web services from the architecture model and selected data transfer methods, and proved the correctness of the algorithm. Furthermore, we developed a tool that provides a graph-based UI for the refactoring and can generate executable prototypes of Web services. To evaluate our method, we conducted case studies for several Web applications and confirmed that the generated prototypes can be used to estimate the performance.
In 2009, the Simple Language of Communicating Objects (Slco) Domain-Specific Language was designed. Since then, a range of tools have been developed around this language to conduct research on a wide range of topics, all related to the construction of complex, component-based software, with formal verification being applied in every development step. In this paper, we present this range, and draw connections between the various, at first glance disparate, research results. We discuss the current status of the Slco framework, i.e., the language in combination with the tools, and plans for future work.
Programmable controllers are gaining prevalence even in distributed safety-critical infrastructures, e.g., in the railway and aerospace industries. Such systems are generally integrated using multiple loosely-coupled reactive components and must satisfy various critical requirements. Thus, their systematic testing is an essential task, which can be encumbered by their distributed characteristics. This paper presents a model-based integration test generation approach leveraging hidden formal methods based on the collaborating statechart models of the components. Statecharts can be integrated using various composition modes (e.g., synchronous and asynchronous) and then transformed (via a symbolic transition systems formalism – XSTS) into the input formalisms of model checker back-ends, namely UPPAAL, Theta and Spin in an automated way. The model checkers are utilized for test generation based on multiple coverage criteria. The approach is implemented in our open source Gamma Statechart Composition Framework and evaluated on industrial-scale distributed controller subsystems from the railway industry.
This paper focuses on generating test cases from timed symbolic transition systems. At the heart of the generation process are symbolic execution techniques on data and time. Test cases look like finite symbolic trees with verdicts on their leaves and are based on a user-specified finite symbolic path playing the role of a test purpose. Generated test cases handle data involved in time constraints and uninitialized parameters, leveraging the advantages of symbolic execution techniques.
The International Symposium on Formal Aspects of Component Software (FACS) was inaugurated two decades ago in response to the major software development paradigm shift from structured development and object-oriented development to component-based software development (CBSD) and service-oriented architecture (SOA). FACS is dedicated to fostering a deeper understanding of the distinctive aspects, promoting research, education, technological advancement, and the practical application of CBSD technology. On the 20th anniversary of FACS, it is appropriate to briefly recall its background and history, thereby highlighting its contributions to the community. Taking this opportunity, we focus on the discussion to elucidate the important aspects of component software that require to be and have been considered in formal theories. Leveraging the refinement of component and object-oriented systems (rCOS) as a framework, we provide an overview of these formal theories and discuss their relationships. We intend to express a vision that different theories and methods are required for different aspects in a CBSD process, and also different formal theories are required even for a particular aspect. However, ensuring their consistent application remains a major challenge and this is a main barrier to the effective industry adoption of CBSD. Furthermore, we delineate emerging challenges and prospects associated with integrating formal methods for modelling and design human-cyber-physical systems (HCPS) - hybrid integration encompassing cyber systems, physical systems, and the mixed human and machine intelligence.
