| 1. |
- Abbasi, Rosa, et al.
(författare)
-
Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeY
- 2023
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 25:2, s. 185-204
-
Tidskriftsartikel (refereegranskat)abstract
- Deductive verification has been successful in verifying interesting properties of real-world programs. One notable gap is the limited support for floating-point reasoning. This is unfortunate, as floating-point arithmetic is particularly unintuitive to reason about due to rounding as well as the presence of the special values infinity and ‘Not a Number’ (NaN). In this article, we present the first floating-point support in a deductive verification tool for the Java programming language. Our support in the KeY verifier handles floating-point arithmetics, transcendental functions, and potentially rounding-type casts. We achieve this with a combination of delegation to external SMT solvers on the one hand, and KeY-internal, rule-based reasoning on the other hand, exploiting the complementary strengths of both worlds. We evaluate this integration on new benchmarks and show that this approach is powerful enough to prove the absence of floating-point special values—often a prerequisite for correct programs—as well as functional properties, for realistic benchmarks.
|
|
| 2. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Language Support for Verifying Reconfigurable Interacting Systems
- 2023
-
Ingår i: International Journal on Software Tools for Technology Transfer (STTT). - 1433-2779 .- 1433-2787.
-
Tidskriftsartikel (refereegranskat)abstract
- Reconfigurable interacting systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. In this article, we provide a modeling and analysis environment for the design of such system. Our tool offers simulation and verification to facilitate native reasoning about the domain concepts of such systems. We present our tool named R-CHECK. R-CHECK supports a high-level input language with matching enumerative and symbolic semantics, and provides a modelling convenience for features such as reconfiguration, coalition formation, self-organisation, etc. For analysis, users can simulate the designed system and explore arising traces. Our included model checker permits reasoning about interaction protocols and joint missions.
|
|
| 3. |
|
|
| 4. |
- Alrahman, Yehia Abd, 1986, et al.
(författare)
-
A distributed API for coordinating AbC programs
- 2020
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 22:4, s. 477-496
-
Tidskriftsartikel (refereegranskat)abstract
- Collective adaptive systems exhibit a particular notion of interaction where environmental conditions largely influence interactions. Previously, we proposed a calculus, named AbC, to model and reason about CAS. The calculus proved to be effective by naturally modelling essential CAS features. However, the question on the tradeoff between its expressiveness and its efficiency, when implemented to program CAS applications, is to be answered. In this article, we propose an efficient and distributed coordination infrastructure for AbC. We prove its correctness, and we evaluate its performance. The main novelty of our approach is that AbC components are infrastructure agnostic. Thus the code of a component does not specify how messages are routed in the infrastructure but rather what properties a target component must satisfy. We also developed a Go API, named GoAt, and an Eclipse plugin to program in a high-level syntax which can be automatically used to generate matching Go code. We showcase our development through a non-trivial case study.
|
|
| 5. |
- De Nicola, Rocco, et al.
(författare)
-
Modelling Flocks of Birds and Colonies of Ants from the Bottom Up
- 2023
-
Ingår i: International Journal on Software Tools for Technology Transfer (STTT). - 1433-2779 .- 1433-2787. ; 25, s. 675-691
-
Tidskriftsartikel (refereegranskat)abstract
- This paper advocates the use of compositional specifications based on formal languages as a means of modelling and analysing sophisticated collective behaviour in natural systems. With the use of appropriate linguistic constructs, models can be developed that are both compact and intuitive, and can be easily refined and extended in small steps. Automated workflows can be implemented on top of this methodology to provide quick feedback, enabling rapid design iterations. To support our argument, we present three examples from the natural world, focusing on flocks of birds and colonies of ants, which feature well-known examples of emergent behaviour in collective adaptive systems. We use an agent-based language to develop simple models that aim at capturing these collective phenomena, and discuss the specific language constructs that we use in the process. Then, we adapt an existing verification tool for the language to simulate our models, and show that our simulations do display emergent behaviour.
|
|
| 6. |
- Gu, Rong, et al.
(författare)
-
Verifiable strategy synthesis for multiple autonomous agents: a scalable approach
- 2022
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Berlin/Heidelberg. - 1433-2779 .- 1433-2787. ; 24:3, s. 395-414
-
Tidskriftsartikel (refereegranskat)abstract
- Path planning and task scheduling are two challenging problems in the design of multiple autonomous agents. Both problems can be solved by the use of exhaustive search techniques such as model checking and algorithmic game theory. However, model checking suffers from the infamous state-space explosion problem that makes it inefficient at solving the problems when the number of agents is large, which is often the case in realistic scenarios. In this paper, we propose a new version of our novel approach called MCRL that integrates model checking and reinforcement learning to alleviate this scalability limitation. We apply this new technique to synthesize path planning and task scheduling strategies for multiple autonomous agents. Our method is capable of handling a larger number of agents if compared to what is feasibly handled by the model-checking technique alone. Additionally, MCRL also guarantees the correctness of the synthesis results via post-verification. The method is implemented in UPPAAL STRATEGO and leverages our tool MALTA for model generation, such that one can use the method with less effort of model construction and higher efficiency of learning than those of the original MCRL. We demonstrate the feasibility of our approach on an industrial case study: an autonomous quarry, and discuss the strengths and weaknesses of the methods.
|
|
| 7. |
- Strandberg, Per Erik, et al.
(författare)
-
Software test results exploration and visualization with continuous integration and nightly testing
- 2022
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : SPRINGER HEIDELBERG. - 1433-2779 .- 1433-2787. ; 24:2, s. 261-285
-
Tidskriftsartikel (refereegranskat)abstract
- Software testing is key for quality assurance of embedded systems. However, with increased development pace, the amount of test results data risks growing to a level where exploration and visualization of the results are unmanageable. This paper covers a tool, Tim, implemented at a company developing embedded systems, where software development occurs in parallel branches and nightly testing is partitioned over software branches, test systems and test cases. Tim aims to replace a previous solution with problems of scalability, requirements and technological flora. Tim was implemented with a reference group over several months. For validation, data were collected both from reference group meetings and logs from the usage of the tool. Data were analyzed quantitatively and qualitatively. The main contributions from the study include the implementation of eight views for test results exploration and visualization, the identification of four solutions patterns for these views (filtering, aggregation, previews and comparisons), as well as six challenges frequently discussed at reference group meetings (expectations, anomalies, navigation, integrations, hardware details and plots). Results are put in perspective with related work and future work is proposed, e.g., enhanced anomaly detection and integrations with more systems such as risk management, source code and requirements repositories.
|
|
| 8. |
- Tan, Yong Kiam, et al.
(författare)
-
Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML
- 2023
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 25:2, s. 167-184
-
Tidskriftsartikel (refereegranskat)abstract
- Modern SAT solvers can emit independently-checkable proof certificates to validate their results. The state-of-the-art proof system that allows for compact proof certificates is propagation redundancy (PR). However, the only existing method to validate proofs in this system with a formally verified tool requires a transformation to a weaker proof system, which can result in a significant blowup in the size of the proof and increased proof validation time. This article describes the first approach to formally verify PR proofs on a succinct representation. We present (i) a new Linear PR (LPR) proof format, (ii) an extension of the DPR-trim tool to efficiently convert PR proofs into LPR format, and (iii) cake_lpr, a verified LPR proof checker developed in CakeML. We also enhance these tools with (iv) a new compositional proof format designed to enable separate (parallel) proof checking. The LPR format is backwards compatible with the existing LRAT format, but extends LRAT with support for the addition of PR clauses. Moreover, cake_lpr is verified using CakeML ’s binary code extraction toolchain, which yields correctness guarantees for its machine code (binary) implementation. This further distinguishes our clausal proof checker from existing checkers because unverified extraction and compilation tools are removed from its trusted computing base. We experimentally show that: LPR provides efficiency gains over existing proof formats; cake_lpr ’s strong correctness guarantees are obtained without significant sacrifice in its performance; and the compositional proof format enables scalable parallel proof checking for large proofs.
|
|
| 9. |
- Yousefi, Farnaz, et al.
(författare)
-
VeriVANca framework : verification of VANETs by property-based message passing of actors in Rebeca with inheritance
- 2020
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : SPRINGER HEIDELBERG. - 1433-2779 .- 1433-2787. ; 22:5, s. 617-633
-
Tidskriftsartikel (refereegranskat)abstract
- Vehicular ad hoc networks have attracted the attention of many researchers during the last years due to the emergence of autonomous vehicles and safety concerns. Most of the frameworks which are proposed for the modeling and analysis VANET applications make use of simulation techniques. Due to the high level of concurrency in these applications, simulation results do not guarantee the correct behavior of the system and more accurate analysis techniques are required. In this paper, we have developed a framework to provide model checking facilities for the analysis of VANET applications. To this end, an actor-based modeling language, Rebeca, is used which is equipped with a variety of model checking engines. We have extended Rebeca with the inheritance mechanism to support model-specific message passing among vehicles, which is crucial for the modeling of VANET applications. To illustrate the applicability of this framework, we modeled and analyzed two warning message dissemination schemes. Reviewing the results of using the model checking technique supports the claim that concurrent behaviors of the system components in VANETs may cause uncertainty which may not be detected by simulation-based techniques. We also observed that considering the interleaving of concurrent executions of the system components affects the performance metrics of it.
|
|
