| 1. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
TriCo—Triple Co-piloting of Implementation, Specification and Tests
- 2022
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 13701 LNCS, s. 174-187, s. 174-187
-
Conference paper (peer-reviewed)abstract
- This white paper presents the vision of a novel methodology for developing safety-critical software, which is inspired by late developments in learning based co-piloting of implementations. The methodology, called TriCo, integrates formal methods with learning based approaches to co-pilot the agile, simultaneous development of three artefacts: implementation, specification, and tests. Whenever the user changes any of these, a TriCo empowered IDE would suggest changes to the other two artefacts in such a way that the three are kept consistent. The user has the final word on whether the changes are accepted, rejected, or modified. In the latter case, consistency will be checked again and re-established. We discuss the emerging trends which put the community in a good position to realise this vision, describe the methodology and workflow, as well as challenges and possible solutions for the realisation of TriCo.
|
|
| 2. |
- Amilon, Jesper, et al.
(author)
-
Deductive Verification Based Abstraction for Software Model Checking
- 2022
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer Nature. ; , s. 7-28
-
Conference paper (peer-reviewed)abstract
- The research community working on formal software verification has historically evolved into two main camps, grouped around two verification methods that are typically referred to as Deductive Verification and Model Checking. In this paper, we present an approach that applies deductive verification to formally justify abstract models for model checking in the TLA framework. We present a proof-of-concept tool chain for C programs, based on Frama-C for deductive verification and TLA+ for model checking. As a theoretical foundation, we summarise a previously developed abstract contract theory as a framework for combining these two methods. Since the contract theory adheres to the principles of contract based design, this justifies the use of the approach in a real-world system design setting. We evaluate our approach on two case studies: a simple C program simulating opening and closing of files, as well as a C program based on real software from the automotive industry.
|
|
| 3. |
- Filipovikj, Predrag, et al.
(author)
-
Bounded Invariant Checking for Stateflow
- 2022
-
In: Electronic Proceedings in Theoretical Computer Science, EPTCS. - : Open Publishing Association. ; , s. 38-52
-
Conference paper (peer-reviewed)abstract
- Stateflow models are complex software models, often used as part of industrial safety-critical software solutions designed with Matlab Simulink. Being part of safety-critical solutions, these models require the application of rigorous verification techniques for assuring their correctness. In this paper, we propose a refutation-based formal verification approach for analyzing Stateflow models against invariant properties, based on bounded model checking (BMC). The crux of our technique is: i) a representation of the state space of Stateflow models as a symbolic transition system (STS) over the symbolic configurations of the model, and ii) application of incremental BMC, to generate verification results after each unrolling of the next-state relation of the transition system. To this end, we develop a symbolic structural operational semantics (SSOS) for Stateflow, starting from an existing structural operational semantics (SOS), and show the preservation of invariant properties between the two. We define bounded invariant checking for STS over symbolic configurations as a satisfiability problem. We develop an automated procedure for generating the initial and next-state predicates of the STS, and a prototype implementation of the technique in the form of a tool utilising standard, off-the-shelf satisfiability solvers. Finally, we present preliminary performance results by applying our tool on an illustrative example and two industrial models.
|
|
| 4. |
- Gurov, Dilian, 1964-, et al.
(author)
-
Alice in Wineland : A Fairy Tale with Contracts
- 2022
-
In: The Logic of Software. A Tasting Menu of Formal Methods. - Cham : Springer Nature. ; , s. 229-242
-
Book chapter (peer-reviewed)abstract
- In this tale Alice ends up in Wineland, where she tries to attend the birthday party of one of its most beloved inhabitants. In order to do so, she must learn about contracts and how important they are. She gets exposed to several contract languages, with their syntax and semantics, such as pre- and post-conditions, state machines, context-free grammars, and interval logic. She learns for what type of properties they are appropriate to use, and how to formally verify that programs meet their contracts.
|
|
| 5. |
- Gurov, Dilian, 1964-, et al.
(author)
-
Knowledge-based strategies for multi-agent teams playing against Nature
- 2022
-
In: Artificial Intelligence. - : Elsevier BV. - 0004-3702 .- 1872-7921. ; 309, s. 103728-
-
Journal article (peer-reviewed)abstract
- We study teams of agents that play against Nature towards achieving a common objective. The agents are assumed to have imperfect information due to partial observability, and have no communication during the play of the game. We propose a natural notion of higher-order knowledge of agents. Based on this notion, we define a class of knowledgebased strategies, and consider the problem of synthesis of strategies of this class. We introduce a multi-agent extension, MKBSC, of the well-known knowledge-based subset construction applied to such games. Its iterative applications turn out to compute higherorder knowledge of the agents. We show how the MKBSC can be used for the design of knowledge-based strategy profiles, and investigate the transfer of existence of such strategies between the original game and in the iterated applications of the MKBSC, under some natural assumptions. We also relate and compare the "intensional" view on knowledge-based strategies based on explicit knowledge representation and update, with the "extensional" view on finite memory strategies based on finite transducers and show that, in a certain sense, these are equivalent.
|
|
| 6. |
- Munoz, D. -J, et al.
(author)
-
Defining categorical reasoning of numerical feature models with feature-wise and variant-wise quality attributes
- 2022
-
In: 26th ACM International Systems and Software Product Line Conference, SPLC 2022 - Proceedings. - New York, NY, USA : Association for Computing Machinery (ACM). ; , s. 132-139
-
Conference paper (peer-reviewed)abstract
- Automatic analysis of variability is an important stage of Software Product Line (SPL) engineering. Incorporating quality information into this stage poses a significant challenge. However, quality-aware automated analysis tools are rare, mainly because in existing solutions variability and quality information are not unified under the same model. In this paper, we make use of the Quality Variability Model (QVM), based on Category Theory (CT), to redefine reasoning operations. We start defining and composing the six most common operations in SPL, but now as quality-based queries, which tend to be unavailable in other approaches. Consequently, QVM supports interactions between variant-wise and feature-wise quality attributes. As a proof of concept, we present, implement and execute the operations as lambda reasoning for CQL IDE - the state-of-the-art CT tool.
|
|
