| 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. |
- Abdulla, Parosh A., et al.
(författare)
-
Parameterized verification
- 2016
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 18:5, s. 469-473
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- The goal of parameterized verification is to prove the correctness of a system specification regardless of the number of its components. The problem is of interest in several different areas: verification of hardware design, multithreaded programs, distributed systems, and communication protocols. The problem is undecidable in general. Solutions for restricted classes of systems and properties have been studied in areas like theorem proving, model checking, automata and logic, process algebra, and constraint solving. In this introduction to the special issue, dedicated to a selection of works from the Parameterized Verification workshop PV '14 and PV '15, we survey some of the works developed in this research area.
|
|
| 5. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Parameterized verification through view abstraction
- 2016
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 18:5, s. 495-516
-
Tidskriftsartikel (refereegranskat)abstract
- We present a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees. Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue. We show that the method is complete for a large class of well quasi-ordered systems including Petri nets. Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. In particular, the method handles the fine-grained and full version of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.
|
|
| 6. |
- Abdulla, Parosh Aziz
(författare)
-
Regular model checking
- 2012
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 14:2, s. 109-118
-
Tidskriftsartikel (refereegranskat)
|
|
| 7. |
|
|
| 8. |
- Abdulla, Parosh, 1961-, et al.
(författare)
-
An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures
- 2017
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : SPRINGER HEIDELBERG. - 1433-2779 .- 1433-2787. ; 19:5, s. 549-563
-
Tidskriftsartikel (refereegranskat)abstract
- We present a technique for automatically verifying safety properties of concurrent programs, in particular programs that rely on subtle dependencies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded number of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state automata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verification, we develop a shape analysis, which tracks correlations between pairs of threads, and a novel abstraction to make the analysis practical. We have implemented our method and used it to verify programs, some of which have not been verified by any other automatic method before.
|
|
| 9. |
- Abdulla, Parosh, et al.
(författare)
-
Regular model checking for LTL(MSO)
- 2012
-
Ingår i: International Journal on Software Tools for Technology Transfer. - Springer : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 14:2, s. 223-241
-
Tidskriftsartikel (refereegranskat)abstract
- Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. We present LTL(MSO), a combination of the logics MSO and LTL as a natural logic for expressing temporal properties to be verified in regular model checking. In other words, LTL(MSO) is a natural specification language for both the system and the property under consideration. LTL(MSO) is a two-dimensional modal logic, where MSO is used for specifying properties of system states and transitions, and LTL is used for specifying temporal properties. In addition, the first-order quantification in MSO can be used to express properties parameterized on a position or process. We give a technique for model checking LTL(MSO), which is adapted from the automata-theoretic approach: a formula is translated to a Buechi regular transition system with a regular set of accepting states, and regular model checking techniques are used to search for models. We have implemented the technique, and show its application to a number of parameterized algorithms from the literature.
|
|
| 10. |
- 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.
|
|
| 11. |
- Amighi, Afshin, et al.
(författare)
-
Provably Correct Control Flow Graphs from Java Bytecode Programs with Exceptions
- 2016
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Nature. - 1433-2779 .- 1433-2787. ; 18:6, s. 653-684
-
Tidskriftsartikel (refereegranskat)abstract
- We present an algorithm for extracting control flow graphs from Java bytecode that captures normal as well as exceptional control flow. We prove its correctness, in the sense that the behaviour of the extracted control flow graph is a sound over-approximation of the behaviour of the original program. This makes control flow graphs suitable for performing various static analyses, such as model checking of temporal safety properties.Analyzing exceptional control flow for Java bytecode is difficult because of the stack-based nature of the language. We therefore develop the extraction in two stages. In the first, we abstract away from the complications arising from exceptional flows, and relativize the extraction on an oracle that is able to look into the stack and predict the exceptions that can be raised at each instruction. This idealized algorithm provides a specification for concrete extraction algorithms, which have to provide a suitable implementation for the oracle. We prove correctness of the idealized algorithm by means of behavioural simulation.In the second stage, we develop a concrete extraction algorithm that consists of two phases. In the first phase, the program is transformed into a BIR program, a stack-less intermediate representation of Java bytecode, from which the control flow graph is extracted in the second phase. We use this intermediate format because it provides the information needed to implement the oracle, and since it gives rise to more compact graphs. We show that the behaviour of the control flow graph extracted via the intermediate representation is a sound over-approximation of the behaviour of the graph extracted by the direct, idealized algorithm, and thus of the original program. The concrete extraction algorithm is implemented as the ConFlEx tool. A number of test cases are performed to evaluate the efficiency of the algorithm.
|
|
| 12. |
- Artho, Cyrille
(författare)
-
Iterative Delta Debugging
- 2011
-
Ingår i: International Journal on Software Tools for Technology Transfer. - 1433-2779 .- 1433-2787. ; 13:3, s. 223-246
-
Tidskriftsartikel (refereegranskat)
|
|
| 13. |
- Aziz Abdulla, Parosh, et al.
(författare)
-
An integrated specification and verification technique for highly concurrent data structures
- 2017
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : SPRINGER HEIDELBERG. - 1433-2779 .- 1433-2787. ; 19:5, s. 549-563
-
Tidskriftsartikel (refereegranskat)abstract
- We present a technique for automatically verifying safety properties of concurrent programs, in particular programs that rely on subtle dependencies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded number of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state automata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verification, we develop a shape analysis, which tracks correlations between pairs of threads, and a novel abstraction to make the analysis practical. We have implemented our method and used it to verify programs, some of which have not been verified by any other automatic method before.
|
|
| 14. |
|
|
| 15. |
- 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.
|
|
| 16. |
- Delzanno, Giorgio, et al.
(författare)
-
A lightweight regular model checking approach for parameterized systems
- 2012
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer-Verlag New York. - 1433-2779 .- 1433-2787. ; 14:2, s. 207-222
-
Tidskriftsartikel (refereegranskat)abstract
- In recent years, we have designed a lightweight approach to regular model checking specifically designed for parameterized systems with global conditions. Our approach combines the strength of regular languages, used for representing infinite sets of configurations, with symbolic model checking and approximations. In this paper, we give a uniform presentation of several variations of a symbolic backward reachability scheme in which different classes of regular expressions are used in place of BDDs. The classification of the proposed methods is based on the precision of the resulting approximated analysis.
|
|
| 17. |
|
|
| 18. |
- Enoiu, Eduard Paul, et al.
(författare)
-
Automated Test Generation using Model-Checking: An Industrial Evaluation
- 2016
-
Ingår i: International Journal on Software Tools for Technology Transfer. - Germany : Springer. - 1433-2779 .- 1433-2787. ; 18:3, s. 335-353
-
Tidskriftsartikel (refereegranskat)abstract
- In software development, testers often focus on functional testing to validate implemented programs against their specifications. In safety critical software development, testers are also required to show that tests exercise, or cover, the structure and logic of the implementation. To achieve different types of logic coverage, various program artifacts such as decisions and conditions are required to be exercised during testing. Use of model-checking for structural test generation has been proposed by several researchers. The limited application to models used in practice and the state-space explosion can, however, impact model-checking and hence the process of deriving tests for logic coverage. Thus, there is a need to validate these approaches against relevant industrial systems such that more knowledge is built on how to efficiently use them in practice. In this paper, we present a tool-supported approach to handle software written in the Function Block Diagram language such that logic coverage criteria can be formalized and used by a model-checker to automatically generate tests. To this end, we conducted a study based on industrial use-case scenarios from Bombardier Transportation AB, showing how our toolbox COMPLETETEST can be applied to generate tests in software systems used in the safety-critical domain. To evaluate the approach, we applied the toolbox to 157 programs and found that it is efficient in terms of time required to generate tests that satisfy logic coverage and scales well for most of the programs.
|
|
| 19. |
- Fantechi, Alessandro, et al.
(författare)
-
Formal methods for railway control systems INTRODUCTION
- 2014
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer. - 1433-2779 .- 1433-2787. ; 16:6, s. 643-646
-
Tidskriftsartikel (refereegranskat)abstract
- The term intelligent transportation systems (ITS) refers to information and communication technology (applied to transport infrastructure and vehicles) that improve transport outcomes such as transport safety, transport productivity, travel reliability, informed travel choices, social equity, environmental performance and network operation resilience. The importance of ITS is increasing as novel driverless/pilotless applications are emerging. This special issue addresses the application of formal methods to model and analyze complex systems in the context of ITS and in particular in the field of railway control systems. In fact, modelling and analysis activities are very important to optimize system life-cycle in the design, development, verification and operational stages, and they are essential whenever assessment and certification is required by international standards. © 2014, Springer-Verlag Berlin Heidelberg.
|
|
| 20. |
- Fredlund, Lars-Åke, et al.
(författare)
-
A tool for verifying software written in Erlang
- 2003. - 1
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 4:4, s. 405-420
-
Tidskriftsartikel (refereegranskat)abstract
- This paper presents an overview of the main results of the project "Verification of Erlang Programs", which is funded by the Swedish Business Development Agency (NUTEK) and by Ericsson within the ASTEC (Advanced Software TEChnology) initiative. Its main outcome is the Erlang Verification Tool (EVT), a theorem prover which assists in obtaining proofs that Erlang applications satisfy their correctness requirements formulated as behavioural properties in a modal logic with recursion. We give a summary of the verification framework as supported by EVT, discuss reasoning principles essential for successful proofs such as inductive and compositional reasoning, and an efficient treatment of side--effect--free code. The experiences of applying the tool in an industrial case study are summarised, and an approach for supporting verification in the presence of program libraries is outlined. EVT is essentially a classical proof assistant, or theorem proving tool, requiring users to intervene in the proof process at crucial steps such as stating program invariants. However, the tool offers considerable support for automatic proof discovery through higher--level tactics tailored to the particular task of the verification of Erlang programs. In addition, a graphical interface permits easy navigation through proof tableaux, proof reuse, and meaningful feedback about the current proof state, to assist users in taking informed proof decisions.
|
|
| 21. |
- Fredlund, Lars-Åke, et al.
(författare)
-
A verification tool for Erlang
- 2003. - 1
-
Ingår i: International Journal on Software Tools for Technology Transfer. - 1433-2779 .- 1433-2787. ; 4:4, s. 405-420
-
Tidskriftsartikel (refereegranskat)abstract
- This paper presents an overview of the main results of the project ``Verification of Erlang Programs'', which is funded by the Swedish Business Development Agency (NUTEK) and by Ericsson within the ASTEC (Advanced Software TEChnology) initiative. Its main outcome is the Erlang Verification Tool EVT, a theorem prover which assists in obtaining proofs that Erlang applications satisfy their correctness requirements formulated as behavioural properties in a modal logic with recursion. We give a summary of the verification framework as supported by EVT, discuss reasoning principles essential for successful proofs such as inductive and compositional reasoning, and an efficient treatment of side-effect-free code. The experiences of applying the tool in an industrial case study are summarised, and an approach for supporting verification in the presence of program libraries is outlined. EVT is essentially a classical proof assistant, or theorem-proving tool, requiring users to intervene in the proof process at crucial steps such as stating program invariants. However, the tool offers considerable support for automatic proof discovery through higher-level tactics tailored to the particular task of the verification of Erlang programs. In addition, a graphical interface permits easy navigation through proof tableaux, proof reuse, and meaningful feedback about the current proof state, to assist users in taking informed proof decisions.
|
|
| 22. |
- Furia, Carlo A, 1979, et al.
(författare)
-
AutoProof: auto-active functional verification of object-oriented programs
- 2017
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 19:6, s. 697-716
-
Tidskriftsartikel (refereegranskat)abstract
- Auto-active verifiers provide a level of automation intermediate between fully automatic and interactive: users supply code with annotations as input while benefiting from a high level of automation in the back-end. This paper presents AutoProof, a state-of-the-art auto-active verifier for object-oriented sequential programs with complex functional specifications. AutoProof fully supports advanced object-oriented features and a powerful methodology for framing and class invariants, which make it applicable in practice to idiomatic object-oriented patterns. The paper focuses on describing AutoProof ’s interface, design, and implementation features, and demonstrates AutoProof ’s performance on a rich collection of benchmark problems. The results attest AutoProof ’s competitiveness among tools in its league on cutting-edge functional verification of object-oriented programs.
|
|
| 23. |
- Ganjei, Zeinab, et al.
(författare)
-
Counting dynamically synchronizing processes
- 2016
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Berlin/Heidelberg. - 1433-2779 .- 1433-2787. ; 18:5, s. 517-534
-
Tidskriftsartikel (refereegranskat)abstract
- We address the problem of automatically establishing correctness for programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. The programs we consider can make use of the shared variables to count and synchronize the spawned processes. This allows them to implement intricate synchronization mechanisms, such as barriers. Automatically verifying correctness, and deadlock freedom, of such programs is beyond the capabilities of current techniques. For this purpose, we make use of counting predicates that mix counters referring to the number of processes satisfying certain properties and variables directly manipulated by the concurrent processes. We then combine existing works on counter, predicate, and constrained monotonic abstraction and build a nested counter example based refinement scheme for establishing correctness (expressed as non-reachability of configurations satisfying counting predicates formulas). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification on several programs whose correctness crucially depends on precisely capturing the number of processes synchronizing using shared variables.
|
|
| 24. |
- 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.
|
|
| 25. |
- Hammarberg, Jerker, et al.
(författare)
-
Formal verification of fault tolerance in safety-critical reconfigurable modules
- 2005
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 7:3, s. 268-279
-
Tidskriftsartikel (refereegranskat)abstract
- Demands for higher flexibility in aerospace applications has led to increasing deployment of reconfiguarble modules. In several cases the industry is looking into Field Programmable Gate Arrays (FPGA) as a means of efficient adaption of existing components. This paper addresses the safety analysis issues for reconfigurable modules with an emphasis on FPGAs. FPGAs act as digital hardware but in the context of safety analysis they should be treated as software, i.e. with added demands on formal analysis. The contributions of this paper are twofold. First, we illustrate a development process using a language with formal semantics (Esterel) for design, formal verification of high-level design, and automatic code generation down to synthesizable VHDL. We argue that this process reduces the likelihood of systematic (permanent) faults in the design, and still produces VHDL code that may be of acceptable quality (size of FPGA, delay). Secondly, in a general approach that is equally applicable to other formal design languages, we illustrate how the effect of transient fault modes and faults in external modules can be formally studied. We modularly extended the component design model with fault models that represent specific or random faults (e.g. radiation leading to bit flips in the component under design), and transient or permanent faults in the rest of the environment. Some faults corrupt inputs to the component and others jeopardise the effect of output signals that control the environment. This process supports a formal version of Failure Modes and Effects Analysis (FMEA). The set-up is then used to formally determine which (single or multiple) fault modes cause violation of the top-level safety-related property, much in the spirit of fault-tree analyses (FTA). All of this is done with out building the fault tree and using a common model for design and for safety analyses. An aerospace hydraulic monitoring system is used to illustrate the analysis of fault tolerance. © Springer-Verlag 2004.
|
|
| 26. |
|
|
| 27. |
|
|
| 28. |
- Khamespanah, Ehsan, et al.
(författare)
-
Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking
- 2018
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : SPRINGER HEIDELBERG. - 1433-2779 .- 1433-2787. ; 20:5, s. 547-561
-
Tidskriftsartikel (refereegranskat)abstract
- Programmers often use informal worst-case analysis and debugging to ensure that schedulers satisfy real-time requirements. Not only can this process be tedious and error-prone, it is inherently conservative and thus likely to lead to an inefficient use of resources. We propose to use model checking to find a schedule which optimizes the use of resources while satisfying real-time requirements. Specifically, we represent a Wireless sensor and actuator network (WSAN) as a collection of actors whose behaviors are specified using a Java-based actor language extended with operators for real-time scheduling and delay representation. We show how the abstraction mechanism and the compositionality of actors in the actor model may be used to incrementally build a model of a WSAN's behavior from node-level and network models. We demonstrate the approach with a case study of a distributed real-time data acquisition system for high-frequency sensing using Timed Rebeca modeling language and the Afra model checking tool.
|
|
| 29. |
- Kokologiannakis, Michalis, et al.
(författare)
-
Stateless model checking of the Linux kernel's read-copy update (RCU)
- 2019
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : SPRINGER HEIDELBERG. - 1433-2779 .- 1433-2787. ; 21:3, s. 287-306
-
Tidskriftsartikel (refereegranskat)abstract
- Read-copy update (RCU) is a synchronization mechanism used heavily in key components of the Linux kernel, such as the virtual filesystem (VFS), to achieve scalability by exploiting RCU's ability to allow concurrent reads and updates. RCU's design is non-trivial, requires a significant effort to fully understand it, let alone become convinced that its implementation is faithful to its specification and provides its claimed properties. The fact that as time goes by Linux kernels are becoming increasingly more complex and are employed in machines with more and more cores and weak memory does not make the situation any easier. This article presents an approach to systematically test the code of the main implementation of RCU used in the Linux kernel (Tree RCU) for concurrency errors, both under sequentially consistent and weak memory. Our modeling allows Nidhugg, a stateless model checking tool, to reproduce, within seconds, safety and liveness bugs that have been reported for RCU. Additionally, we present the real cause behind some failures that have been observed in production systems in the past. More importantly, we were able to verify both the publish-subscribe and the grace-period guarantee, with the latter being the basic and most important guarantee that RCU offers, on several Linux kernel versions, for particular configurations. Our approach is effective, both in dealing with the increased complexity of recent Linux kernels and in terms of time that the process requires. We hold that our effort constitutes a good first step toward making tools such as Nidhugg part of the standard testing infrastructure of the Linux kernel.
|
|
| 30. |
|
|
| 31. |
- Larsen, Kim Guldstrand, et al.
(författare)
-
UPPAAL in a nutshell
- 1997
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 1:1-2, s. 134-152
-
Tidskriftsartikel (refereegranskat)
|
|
| 32. |
|
|
| 33. |
- Lisper, Björn, et al.
(författare)
-
Practical experiences of applying source-level WCET flow analysis to industrial code
- 2013
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 15:1, s. 53-63
-
Tidskriftsartikel (refereegranskat)abstract
- Code-level timing analysis, such as worst-case execution time (WCET) analysis, usually takes place at the binary level. However, many program properties that are important for the analysis, such as constraints on possible program flows, are easier to derive at the source code level since this code contains much more information. Therefore, various source-level analyses can provide valuable support for timing analysis. However, source-level analysis is not always smoothly applicable in industrial settings. In this paper, we report on the experiences of applying source-level analysis to industrial code in the ALL-TIMES project: the promises, the pitfalls, and the workarounds that were developed. We also discuss various approaches to how the difficulties that were encountered can be tackled.
|
|
| 34. |
- Lisper, Björn
(författare)
-
The ALL-TIMES project : Introduction and overview
- 2013
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 15:1, s. 1-8
-
Tidskriftsartikel (refereegranskat)abstract
- Timing analysis is important when designing and verifying time-critical embedded systems. Tool support for timing analysis has existed for a number of years, but the tools have been mostly working in isolation resulting in less efficient timing analysis processes. The European FP7 project ALL-TIMES has addressed this issue by creating interface formats, tool chains, and integrated methodologies for timing analysis where the proper combination of tools and techniques can be used in a given situation. We give an introduction and overview of the ALL-TIMES project: its objectives, tools and partners, work done, and the results.
|
|
| 35. |
- Margaria, Tiziana, et al.
(författare)
-
Scalability aspects of validation
- 2003
-
Ingår i: International Journal on Software Tools for Technology Transfer. - 1433-2779 .- 1433-2787. ; 5:1
-
Tidskriftsartikel (refereegranskat)
|
|
| 36. |
- Marrone, Stefano, et al.
(författare)
-
Towards Model-Driven V&V assessment of railway control systems
- 2014
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer. - 1433-2779 .- 1433-2787. ; 16:6, s. 669-683
-
Tidskriftsartikel (refereegranskat)abstract
- Verification and Validation (V&V) activities aiming at certifying railway controllers are among the most critical and time-consuming in system development life cycle. As such, they would greatly benefit from novel approaches enabling both automation and traceability for assessment purposes. While several formal and Model-Based approaches have been proposed in the scientific literature, some of which are successfully employed in industrial settings, we are still far from an integrated and unified methodology which allows guiding design choices, minimizing the chances of failures/non-compliances, and considerably reducing the overall assessment effort. To address these issues, this paper describes a Model-Driven Engineering approach which is very promising to tackle the aforementioned challenges. In fact, the usage of appropriate Unified Modeling Language profiles featuring system analysis and test case specification capabilities, together with tool chains for model transformations and analysis, seems a viable way to allow end-users to concentrate on high-level holistic models and specification of non-functional requirements (i.e., dependability) and support the automation of the V&V process. We show, through a case study belonging to the railway signalling domain, how the approach is effective in supporting activities like system testing and availability evaluation. © 2014, Springer-Verlag Berlin Heidelberg.
|
|
| 37. |
- Merriam, N., et al.
(författare)
-
Estimation of productivity increase for timing analysis tool chains
- 2013
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 15:1, s. 65-84
-
Tidskriftsartikel (refereegranskat)abstract
- Within the scope of the ALL-TIMES project, not only were tool interfaces designed and implemented but also new, powerful timing analysis methodologies constructed. To gauge the effectiveness of these results we used a number of methods to assess the productivity increase that would be achieved by introducing the new techniques. We collect and report on the conclusions of these assessments. © 2012 Springer-Verlag.
|
|
| 38. |
- Nilsson, Agneta, 1968, et al.
(författare)
-
Assessing the effects of introducing a new software development process: a methodological description
- 2015
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 17, s. 1-16
-
Tidskriftsartikel (refereegranskat)abstract
- © 2013, Springer-Verlag Berlin Heidelberg. In this article, we report from a 22-months long action research study in which we evaluate the usefulness of a set of software development tools in an industrial setting, a small software company. We focus on how developers in the industry use and adopt these tools, what expectations they have on them, how the tools can be improved, and how the adoption process itself can be improved. We describe these change processes from a methodological perspective, how we monitored the processes, how we reviewed the outcomes, and the strategies that we applied. We show how the processes evolved, intermediate results, and the steps that were taken along the way based on the outcomes. We believe that the described study may inspire other tool-developers and/or researchers to organize similar studies to further our understanding of the complex processes involved in the adoption of software development tools in industry.
|
|
| 39. |
- 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.
|
|
| 40. |
- 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.
|
|
| 41. |
- Wong, Peter Y. H., et al.
(författare)
-
Testing abstract behavioral specifications
- 2014
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer. - 1433-2779 .- 1433-2787. ; 17:1, s. 107-119
-
Tidskriftsartikel (refereegranskat)abstract
- We present a range of testing techniques for the Abstract Behavioral Specification (ABS) language and apply them to an industrial case study. ABS is a formal modeling language for highly variable, concurrent, component-based systems. The nature of these systems makes them susceptible to the introduction of subtle bugs that are hard to detect in the presence of steady adaptation. While static analysis techniques are available for an abstract language such as ABS, testing is still indispensable and complements analytic methods. We focus on fully automated testing techniques including black-box and glass-box test generation as well as runtime assertion checking, which are shown to be effective in an industrial setting.
|
|
| 42. |
- 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.
|
|
| 43. |
|
|
