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.
