Search

This special issue of Software Tools for Technology Transfer comprises extended versions of selected papers from the 26th edition of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020). The focus of this conference series is tools and algorithms for the rigorous analysis of software and hardware systems, and the papers in this special cover the spectrum of current work in this field. [ABSTRACT FROM AUTHOR]

This special issue of Software Tools for Technology Transfer presents extended versions of two selected papers from the 23rd edition of TACAS, the International Conference on Tools and Algorithms for the Construction and Analysis of Systems that took place in April 2017 in Uppsala. The papers included in this special issue concern various aspects of automated design and formal verification; they therefore contribute to the development of more reliable computer systems. [ABSTRACT FROM AUTHOR]

Software systems are complicated, and the scientific and engineering methodologies for software development are relatively young. Cyber-physical systems are now in every corner of our lives, and we need robust methods for handling the ever-increasing complexity of their software systems. Model-Driven Development is a promising approach to tackle the complexity of systems through the concept of abstraction, enabling analysis at earlier phases of development. In this paper, we propose a model-driven approach with a focus on guaranteeing safety using formal verification. Cyber-physical systems are distributed, concurrent, asynchronous and event-based reactive systems with timing constraints. The actor-based textual modeling language, Rebeca, with model checking support is used for formal verification. Starting from structured requirements and system architecture design the behavioral models, including Rebeca models, are built. Properties of interest are also derived from the structured requirements, and then model checking is used to formally verify the properties. This process can be performed in iterations until satisfaction of desired properties are ensured, and possible ambiguities and inconsistencies in requirements are resolved. The formally verified models can then be used to develop the executable code. The Rebeca models include the details of the signals and messages that are passed at the network level including the timing, and this facilitates the generation of executable code. The natural mappings among the models for requirements, the formal models, and the executable code improve the effectiveness and efficiency of the approach. [ABSTRACT FROM AUTHOR]

Programmable logic controllers (PLCs) are heavily used in industrial control systems, because of their high capacity of simultaneous input/output processing capabilities. Characteristically, PLC systems are used in mission critical systems, and PLC software needs to conform real-time constraints in order to work properly. Since PLC programming requires mastering low-level instructions or assembly like languages, an important step in PLC software production is modelling using a formal approach like Petri nets or automata. Afterward, PLC software is produced semiautomatically from the model and refined iteratively. Model checking, on the other hand, is a well-known software verification approach, where typically a set of timed properties are verified by exploring the transition system produced from the software model at hand. Naturally, model checking is applied in a variety of ways to verify the correctness of PLC-based software. In this paper, we provide a broad view about the difficulties that are encountered during the model checking process applied at the verification phase of PLC software production. We classify the approaches from two different perspectives: first, the model checking approach/tool used in the verification process, and second, the software model/source code and its transformation to model checker's specification language. In a nutshell, we have mainly examined SPIN, SMV, and UPPAAL-based model checking activities and model construction using Instruction Lists (and alike), Function Block Diagrams, and Petri nets/automata-based model construction activities. As a result of our studies, we provide a comparison among the studies in the literature regarding various aspects like their application areas, performance considerations, and model checking processes. Our survey can be used to provide guidance for the scholars and practitioners planning to integrate model checking to PLC-based software verification activities. [ABSTRACT FROM AUTHOR]

Model checking is a formal verification technique. It takes an exhaustively strategy to check hardware circuits and network protocols against desired properties. Having been developed for more than three decades, model checking is now playing an important role in software engineering for verifying rather complicated software artifacts.This paper surveys the role of model checking in software engineering. In particular, we searched for the related literatures published at reputed conferences, symposiums, workshops, and journals, and took a survey of (1) various model checking techniques that can be adapted to software development and their implementations, and (2) the use of model checking at different stages of a software development life cycle. We observed that model checking is useful for software debugging, constraint solving, and malware detection, and it can help verify different types of software systems, such as object- and aspect-oriented systems, service-oriented applications, web-based applications, and GUI applications including safety- and mission-critical systems.The survey is expected to help human engineers understand the role of model checking in software engineering, and as well decide which model checking technique(s) and/or tool(s) are applicable for developing, analyzing and verifying a practical software system. For researchers, the survey also points out how model checking has been adapted to their research topics on software engineering and its challenges. [ABSTRACT FROM AUTHOR]

Summary: The automation of programming, which lies at the intersection of software engineering and artificial intelligence, enables machines to automatically generate programs that satisfy given requirements. In the context of B formal design modeling, one of the challenges is the refactoring of substitutions in design specifications, which often uses state transitions to describe how program or system statuses change during execution. This paper proposes a condition and substitution refactoring algorithm for the B formal specification language. The aim of the work is to automatically derive B operational predicates based on given transitions. The work has been extremely useful to machine‐driven formal design model repair as well as automated design specification generation. Given a set of state transitions, common relations of their state variables can be discovered and clustered into a number of classes. These relations can be further used to synthesize substitutions that derive new states from existing states. To restrict application domains of the synthesized substitutions, conditions that guard these substitutions are generated using first‐order logic. We have implemented the proposed algorithm as an extension to the ProB model checker. Experiments were conducted based on the B model public dataset. The evaluation results demonstrated that our solution is able to synthesize conditions and substitutions for various sets of state transitions in a wide range of B models. [ABSTRACT FROM AUTHOR]

The first attempts to apply the k-induction method to software verification are only recent. In this paper, we present a novel proof by induction algorithm, which is built on the top of a symbolic context-bounded model checker and uses an iterative deepening approach to verify, for each step k up to a given maximum, whether a given safety property $$\phi $$ holds in the program. The proposed k-induction algorithm consists of three different cases, called base case, forward condition, and inductive step. Intuitively, in the base case, we aim to find a counterexample with up to k loop unwindings; in the forward condition, we check whether loops have been fully unrolled and that $$\phi $$ holds in all states reachable within k unwindings; and in the inductive step, we check that whenever $$\phi $$ holds for k unwindings, it also holds after the next unwinding of the system. The algorithm was implemented in two different ways, a sequential and a parallel one, and the results were compared. Experimental results show that both forms of the algorithm can handle a wide variety of safety properties extracted from standard benchmarks, ranging from reachability to time constraints. And by comparison, the parallel algorithm solves more verification tasks in less time. This paper marks the first application of the k-induction algorithm to a broader range of C programs; in particular, we show that our k-induction method outperforms CPAChecker in terms of correct results, which is a state-of-the-art k-induction-based verification tool for C programs. [ABSTRACT FROM AUTHOR]

Even with impressive advances in formal methods, certain major challenges remain. Chief among these are environment modeling, incompleteness in specifications, and the hardness of underlying decision problems. In this paper, we characterize two trends that show great promise in meeting these challenges. The first trend is to perform verification by reduction to synthesis. The second is to solve the resulting synthesis problem by integrating traditional, deductive methods with inductive inference (learning from examples) using hypotheses about system structure. We present a formalization of such an integration, show how it can tackle hard problems in verification and synthesis, and outline directions for future work. [ABSTRACT FROM AUTHOR]

Finite-state models, such as finite-state machines (FSMs), aid software engineering in many ways. They are often used in formal verification and also can serve as visual software models. The latter application is associated with the problems of software synthesis and automatic derivation of software models from specification. Smaller synthesized models are more general and are easier to comprehend, yet the problem of minimum FSM identification has received little attention in previous research. This paper presents four exact methods to tackle the problem of minimum FSM identification from a set of test scenarios and a temporal specification represented in linear temporal logic. The methods are implemented as an open-source tool. Three of them are based on translations of the FSM identification problem to SAT or QSAT problem instances. Accounting for temporal properties is done via counterexample prohibition. Counterexamples are either obtained from previously identified FSMs, or based on bounded model checking. The fourth method uses backtracking. The proposed methods are evaluated on several case studies and on a larger number of randomly generated instances of increasing complexity. The results show that the Iterative SAT-based method is the leader among the proposed methods. The methods are also compared with existing inexact approaches, i.e., the ones which do not necessarily identify the minimum FSM, and these comparisons show encouraging results. [ABSTRACT FROM AUTHOR]

The worldwide mobile software market has grown dramatically since feature phones became popular in the early 1990s. In practice, mobile usability - which can be defined for a resource-constrained device in two ways, namely, User eXperience (UX) and User Interface (UI) - has been regarded as the key to gaining superiority in terms of both market share and customer loyalty. Unfortunately, de facto standards for software design and the development process, such as Unified Modeling Language (UML) and Rational Unified Process (RUP), do not seem to promote mobile usability in a systematic manner in practice. This paper proposes a systematic and generalizable approach to modeling and evaluating the properties of mobile usability, herein treating it as a first-class software quality from the perspective of software engineering. We devise a UX evaluation framework for mobile usability, which we call UX Evaluation Framework (UEF) throughout this paper. A UX is specified by inter-scene interactions between users and terminals of software products using Extended Menu Navigation Viewpoints (EMNVs); then, a model checker, NuSMV, is adopted to observe whether the EMNV model meets a set of given UX properties. Importantly, the analysis and design of RUP is extended to support the co-design of UX and UI so that major roles, activities and artifacts in the UX and UI can be explicitly monitored and controlled by stakeholders. Through case studies, we demonstrate that UEF works properly to treat software products that prioritize mobile usability. Consequently, UEF plays a key role in filling the gap between two research disciplines to address usability: software engineering and human-computer interactions. [ABSTRACT FROM AUTHOR]

The emergence of collective adaptive systems—i.e., computational systems made up of an ensemble of autonomous components that have to operate in a coordinated and adaptive way in open-ended and unpredictable environments—calls for innovative modeling and software engineering tools, to support their systematic and rigorous design and development. In this paper, we present a general model for collective adaptive systems called SOTA ("State Of The Affairs"). SOTA brings together the lessons of goal-oriented requirements modeling, context-aware system modeling, and dynamical systems modeling. It has the potential for acting as a general reference model to help tackling some key issues in the design and development of collective adaptive systems. In particular, as we will show with reference to a scenario of collectives of autonomous vehicles, SOTA enables: early verification of requirements, identification of knowledge requirements for self-adaptation, and the identification of the most suitable architectural patterns for self-adaptation. [ABSTRACT FROM AUTHOR]

With the increasing complexity of the problems and systems arising nowadays, the use of multi-level models is becoming more frequent in practice. However, there are still few reports in the literature concerning methods for analyzing such models without flattening the multi-level structure. For instance, several variants of multi-level Petri nets have been applied for modeling interaction protocols and mobility in multi-agent systems and coordination of cross-organizational workflows. But there are few automated tools for analyzing the behavior of these nets. In this paper we explain how to detect faults in models based on a representative class of multi-level nets: the nested Petri nets. We translate a nested net into a verifiable model that preserves its modular structure, a PROMELA program. This allows the use of SPIN model checker to verify properties related to termination, boundedness and reachability. [ABSTRACT FROM AUTHOR]

Relational algebra offers to software engineering the same degree of conciseness and calculational power as linear algebra in other engineering disciplines. Binary relations play the role of matrices with similar emphasis on multiplication and transposition. This matches with Alloy's lemma “everything is a relation” and with the relational basis of the Algebra of Programming (AoP). Altogether, it provides a simple and coherent approach to checking and calculating programs from abstract models. In this paper, we put Alloy and the Algebra of Programming together in a case study originating from the Verifiable File System mini-challenge put forward by Joshi and Holzmann: verifying the refinement of an abstract file store model into a journaled (Flash) data model catering to wear leveling and recovery from power loss. Our approach relies on diagrams to graphically express typed assertions. It interweaves model checking (in Alloy) with calculational proofs in a way which offers the best of both worlds. This provides ample evidence of the positive impact in software verification of Alloy's focus on relations, complemented by induction-free proofs about data structures such as stores and lists. [ABSTRACT FROM PUBLISHER]

Secure software engineering is a new research area that has been proposed to address security issues during the development of software systems. This new area of research advocates that security characteristics should be considered from the early stages of the software development life cycle and should not be added as another layer in the system on an ad-hoc basis after the system is built. In this paper, we describe a UML-based Static Verification Framework (USVF) to support the design and verification of secure software systems in early stages of the software development life-cycle taking into consideration security and general requirements of the software system. USVF performs static verification on UML models consisting of UML class and state machine diagrams extended by an action language. We present an operational semantics of UML models, define a property specification language designed to reason about temporal and general properties of UML state machines using the semantic domains of the former, and implement the model checking process by translating models and properties into Promela, the input language of the SPIN model checker. We show that the methodology can be applied to the verification of security properties by representing the main aspects of security, namely availability, integrity and confidentiality, in the USVF property specification language. [ABSTRACT FROM AUTHOR]

Graph Grammars have recently become more and more popular as a general formal modeling language. Behavioral modeling of dynamic systems and model to model transformations are a few well-known examples in which graphs have proven their usefulness in software engineering. A special type of graph transformation systems is layered graphs. Layered graphs are a suitable formalism for modeling hierarchical systems. However, most of the research so far concentrated on graph transformation systems as a modeling means, without considering the need for suitable analysis tools. In this paper we concentrate on how to analyze these models. We will describe our approach to show how one can verify the designed graph transformation systems. To verify graph transformation systems we use a novel approach: using Bogor model checker to verify graph transformation systems. The AGG-like graph transformation systems are translated to BIR — the input language of Bogor — and Bogor verifies that model against some properties defined by combining LTL and special purpose graph rules. Supporting schema-based and layered graphs characterize our approach among existing solutions for verification of graph transformation systems. [ABSTRACT FROM AUTHOR]

Software and system dependability is getting ever more important in embedded system design. Current industrial practice of model-based analysis is supported by state-transition diagrammatic notations such as Statecharts. State-of-the-art modeling tools like STATEMATE support safety and failure-effect analysis at design time, but restricted to qualitative properties, This paper reports on a (plug-in) extension of STATEMATE enabling the evaluation of quantitative dependability properties at design time. The extension is compositional in the way the model is augmented with probabilistic timing information. This fact is exploited in the construction of the underlying mathematical model, a uniform continuous-time Markov decision process, on which we are able to check requirements of the form: "The probability to hit a safety-critical system configuration within a mission time of 3 hours is at most 0.01." We give a detailed explanation of the construction and evaluation steps making this possible, and report on a nontrivial case study of a high- speed train signaling system where the tool has been applied successfully. [ABSTRACT FROM AUTHOR]

Providing evidence for the refutation of a property is an essential, if not the most important, feature of model checking. This paper considers algorithms for counterexample generation for probabilistic CTL formulas in discrete-time Markov chains. Finding the strongest evidence (i.e., the most probable path) violating a (bounded) until-formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that deviate most from the required probability bound can be obtained by applying (small amendments to) k-shortest (hop-constrained) paths algorithms. These results can be extended to Markov chains with rewards, to LTL model checking, and are useful for Markov decision processes. Experimental results show that, typically, the size of a counterexample is excessive. To obtain much more compact representations, we present a simple algorithm to generate (minimal) regular expressions that can act as counterexamples. The feasibility of our approach is illustrated by means of two communication protocols: leader election in an anonymous ring network and the Crowds protocol. [ABSTRACT FROM AUTHOR]

This paper presents a lightweight interval analysis technique for determining the lower and upper bounds for program variables and its application in improving software model checking techniques. The experiments demonstrate that it is an effective approach to alleviate the state explosion problem in software model checking. [ABSTRACT FROM AUTHOR]

In this paper, we investigate the problem of configuration verification for the extended FSM (EFSM) model. This is an extension of the FSM state identification problem. Specifically, given a configuration ("state vector") and an arbitrary set of configurations, determine an input sequence such that the EFSM in the given configuration produces an output sequence different from that of the configurations in the given set or at least in a maximal proper subset. Such a sequence can be used in a test case to confirm the destination configuration of a particular EFSM transition. We demonstrate that this problem could be reduced to the EFSM traversal problem, so that the existing methods and tools developed in the context of model checking become applicable. We introduce notions of EFSM projections and products and, based on these notions, we develop a theoretical framework for determining configuration-confirming sequences. The proposed approach is illustrated on a realistic example. [ABSTRACT FROM AUTHOR]

Temporal logic query checking was first introduced by W. Chan in order to speed up design understanding by discovering properties not known a priori. A query is a temporal logic formula containing a special symbol ?1, known as a placeholder. Given a Kripke structure and a propositional formula δ, we say that δ satisfies the query if replacing the placeholder by δ results in a temporal logic formula satisfied by the Kripke structure. A solution to a temporal logic query on a Kripke structure is the set of all propositional formulas that satisfy the query. Query checking helps discover temporal properties of a system and, as such, is a useful tool for model exploration. In this paper, we show that query checking is applicable to a variety of model exploration tasks, ranging from invariant computation to test case generation. We illustrate these using a Cruise Control System. Additionally, we show that query checking is an instance of a multi-valued model checking of Chechik et al. This approach enables us to build an implementation of a temporal logic query checker, TLQSolver, on top of our existing multi-valued model checker χChek. It also allows us to decide a large class of queries and introduce witnesses for temporal logic queries--an essential notion for effective model exploration. [ABSTRACT FROM AUTHOR]

We report an error in a verification model in [41 and present a revised model with verification result. Our result explains the reason why SPIN found the race condition in the synchronization algorithm. We also show that the suggested fix in [4] is incorrect. [ABSTRACT FROM AUTHOR]

A Mix Net is a cryptographic protocol that unlinks the correspondence between its inputs and its outputs. In this paper, we formally analyse a Mix Net using the process algebra CSP and its associated model checker FDR. The protocol that we verify removes the reliance on a Web Bulletin Board: rather than communicating via a Web Bulletin Board, the protocol allows the mix servers to communicate directly, exchanging signed messages and maintaining their own records of the messages they have received. Mix Net analyses in the literature are invariably focused on safety properties; important liveness properties, such as deadlock freedom, are wholly neglected. This is an unhappy omission, however, since a Mix Net that produces no results is of little use. In contrast, we verify here that the Mix Net is guaranteed to terminate, with each honest mix server outputting the decrypted vector of plaintexts alongside a chain proving that each re-encryption/permutation and partial decryption operation was performed correctly, under the assumption that there is an honest majority of them acting according to the protocol. [ABSTRACT FROM AUTHOR]

Equivalence checking plays a crucial role in formal verification since it is a natural relation for expressing the matching of a system implementation against its specification. In this paper, we present an efficient procedure, based on heuristic search, for checking well-known bisimulation equivalences for concurrent systems specified through process algebras. The method tries to improve, with respect to other solutions, both the memory occupation and the time required for proving the equivalence of systems. A prototype has been developed to evaluate the approach on several examples of concurrent system specifications. [ABSTRACT FROM AUTHOR]

This paper describes ProMoVer, a tool for fully automated procedure-modular verification of Java programs equipped with method-local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure-level is a natural instantiation of the modular verification paradigm, where correctness of global properties is relativized on the local properties of the methods rather than on their implementations. Here, it is based on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositional verification of control flow safety properties, and provides appropriate pre- and post-processing. Both linear-time temporal logic and finite automata are supported as formalisms for expressing local and global safety properties, allowing the user to choose a suitable format for the property at hand. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes in the code and the specifications. The verification task is relatively light-weight due to support for abstraction from private methods and automatic extraction of candidate specifications from method implementations. We evaluate the tool on a number of applications from the domains of Java Card and web-based application. [ABSTRACT FROM AUTHOR]

Abstract: Controllers in safety critical systems such as nuclear power plants often use the Function Block Diagram (FBD) to design software embedded in the PLC (Programmable Logic Controller). Software engineers develop FBD programs manually, while engineering tools provided by PLC vendors translate them into ANSI-C programs mechanically. Every new PLC and its software engineering tool should demonstrate the so-called FBD-to-C translator's correctness thoroughly. This paper proposes a verification process which can efficiently verify the translator's correctness using the model checking technique. The HW-CBMC model checker verifies the behavioral consistency between FBD and ANSI-C programs formally according to the process and templates which this paper proposes. We also developed a CASE tool ‘CWrapper’ and performed a case study with simplified examples of the APR-1400 (Advanced Power Reactor-1400) nuclear reactor protection system in Korea. [Copyright &y& Elsevier]

Firewalls are crucial for the security of most networks and implemented by packet filters. Those packet filters can be considered the direct opposite of a simple-to-use system. Configured with complex commands in plain text files, only experts are able to understand or even modify such a setup. Recently, this process has been improved by using a combination of external tools, a graphical modeling environment, and a model checker, enabling more users to participate in the process and clearing the way to automatic testing. This paper revists this concept from a simplicity perspective and shows how the whole process can be simplified while simultaneously the level of abstraction is increased and new ways of verifying the result are possible. [ABSTRACT FROM AUTHOR]

The process of Requirements Engineering (RE) includes many activities, from goal elicitation to requirements specification. The aim is to develop an operational requirements specification that is guaranteed to satisfy the goals. In this paper, we propose a formal, systematic approach for generating a set of operational requirements that are complete with respect to given goals. We show how the integration of model checking and inductive learning can be effectively used to do this. The model checking formally verifies the satisfaction of the goals and produces counterexamples when incompleteness in the operational requirements is detected. The inductive learning process then computes operational requirements from the counterexamples and user-provided positive examples. These learned operational requirements are guaranteed to eliminate the counterexamples and be consistent with the goals. This process is performed iteratively until no goal violation is detected. The proposed framework is a rigorous, tool-supported requirements elaboration technique which is formally guided by the engineer's knowledge of the domain and the envisioned system. [ABSTRACT FROM PUBLISHER]

This paper introduces a novel framework for Ontology-Driven Software Engineering. This framework is grounded on the prior related work that studied the interplay between the model-driven engineering and the ontological modeling. Our framework makes a contribution by incorporating a more flexible means for ontological modeling that also has a higher performance in processing, and by incorporating a wider range of ontology types into ODSE. As a result, it extends the power and speed of the classification and the model consistency checking ontological services enabled by the prior work, and brings new ontological services: semantic search in model repositories, three kinds of semi-automated model composition services: task-based, result-based, and opportunistic, and the policy enforcement service. The primary intended use for this framework is to be implemented as part of model-driven engineering tools to support software engineers. We describe our reference implementation of such a tool called Smart Modeller, and report on a performance evaluation of our framework carried out with the help of it. [ABSTRACT FROM AUTHOR]

In this paper, we present a unified approach for the verification and validation of software and systems engineering design models expressed in UML 2.0 and SysML 1.0. The approach is based on three well-established techniques, namely formal analysis, programme analysis and software engineering (SwE) techniques. More precisely, our contribution consists of the synergistic combination of model checking, static analysis and SwE metrics that enables the automatic and efficient assessment of design models from static and dynamic perspectives. Additionally, we present the design and implementation of an automated computer-aided assessing framework integrating the proposed approach. Moreover, we discuss the related technical details and the underlying synergism. Finally, we illustrate the proposed approach by assessing a design case study that is composed of state machine and sequence diagrams. [ABSTRACT FROM AUTHOR]

Model checking is an efficient formal verification technique that has been applied to a wide spectrum of applications in software engineering. Popular model checking algorithms include Bounded Model Checking (BMC) and Incremental Construction of Inductive Clauses for Indubitable Correctness/Property Directed Reachability(IC3/PDR). The recently proposed Complementary Approximate Reachability (CAR) model checking algorithm has a performance close to BMC in bug-finding, while its depth-first strategy sometimes leads the algorithm to a trap, which will waste lots of computation. In this paper, we enhance the recently proposed Complementary Approximate Reachability (CAR) model checking algorithm by integrating the restart policy, which yields a restartable CAR model (abbreviated as r-CAR). The restart policy can help avoid the trap problem caused by the depth-first strategy and has played an important role in modern SAT-solving algorithms to search for a satisfactory solution. As the bug-finding in model checking is reducible to a similar search problem, the restart policy can be useful to enhance the bug-finding capability. We made an extensive experiment to evaluate the new algorithm. Our results show that out of the 749 industrial instances, r-CAR is able to find 13 instances that the state-of-the-art BMC technique cannot find and can solve more than 11 instances than the original CAR. The new algorithm successfully contributes to the current model-checking portfolio in practice. [ABSTRACT FROM AUTHOR]

Abstract The increasing level of automation in critical infrastructures requires development of effective ways for finding faults in safety critical software components. Synchronization in concurrent components is especially prone to errors and, due to difficulty of exploring all thread interleavings, it is difficult to find synchronization faults. In this paper we present an experimental study demonstrating the effectiveness of model checking techniques in finding synchronization faults in safety critical software when they are combined with a design for verification approach. We based our experiments on an automated air traffic control software component called the Tactical Separation Assisted Flight Environment (TSAFE). We first reengineered TSAFE using the concurrency controller design pattern. The concurrency controller design pattern enables a modular verification strategy by decoupling the behaviors of the concurrency controllers from the behaviors of the threads that use them using interfaces specified as finite state machines. The behavior of a concurrency controller is verified with respect to arbitrary numbers of threads using the infinite state model checking techniques implemented in the Action Language Verifier (ALV). The threads which use the controller classes are checked for interface violations using the finite state model checking techniques implemented in the Java Path Finder (JPF). We present techniques for thread isolation which enables us to analyze each thread in the program separately during interface verification. We conducted two sets of experiments using these verification techniques. First, we created 40 faulty versions of TSAFE using manual fault seeding. During this exercise we also developed a classification of faults that can be found using the presented design for verification approach. Next, we generated another 100 faulty versions of TSAFE using randomly seeded faults that were created automatically based on this fault classification. We used both infinite and finite state verification techniques for finding the seeded faults. The results of our experiments demonstrate the effectiveness of the presented design for verification approach in eliminating synchronization faults. [ABSTRACT FROM AUTHOR]

We investigate the benefits of using a synchronous data-flow language for programming critical real-time systems. These benefits concern ergonomy—since the dataflow approach meets traditional description tools used in this domain—and ability to support formal design and verification methods. We show, on a simple example, how the language LUSTRE, and its associated verification tool LESAR, can be used to design a program, to specify its critical properties, and to verify these properties. As the language LUSTRE and its uses have already been published in several papers (e.g., [11], [18]), we put particular emphasis on program verification. A preliminary version of this paper has been published in [28]. [ABSTRACT FROM AUTHOR]

In this paper, we demonstrate how model checking can be used to verify safety properties for event-driven systems. SCR tabular requirements describe required system behavior in a format that is intuitive, easy to read, and scalable to large systems (e.g., the software requirements for the A7 aircraft). Model checking of temporal logics has been established as a sound technique for verifying properties of hardware systems. We have developed an automated technique for formalizing the semiformal SCR requirements and for transforming the resultant formal specification onto a finite structure that a model checker can analyze. This technique was effective in uncovering violations of system invariants in both an automobile cruise control system and a water-level monitoring system. [ABSTRACT FROM AUTHOR]

Software architectural style is one of the best concepts to define a family of related architectures and their common properties. Despite the essential role of software architectures in the software engineering practice, the lack of formal description and analysis may hamper the quality of designed models. Hence, using proper formal languages seems necessary for architectural style description. In this case, it is possible to use model checking to verify the designed models automatically. However, the model checking of complex software systems suffers from the state space explosion problem. To handle this problem, data mining techniques may contribute to obtain the required knowledge for intelligent model checking i.e. searching only a portion of the state space. In this paper, to check the model of complex software systems which are designed according to an architectural style, an efficient approach is proposed using data mining techniques. These software systems must be specified through architectural styles and modeled by Graph Transformation Systems (GTS) formally. In the proposed approach, to check a large model based on a specific style intelligently, a specific knowledge is required. Such knowledge is acquired from mining the data of checking a smaller model consistent with the same style. These smaller models can be designed either by the designers or can be automatically generated consistent with the style. The proposed solution can be used to verify the reachability property and to refute the safety and liveness properties. This solution is implemented in GROOVE, a toolset for designing and model checking of graph transformation systems. The experimental results show that our method is faster and more accurate in comparison with the existing techniques in model checking of complex software systems. [ABSTRACT FROM AUTHOR]

Abstract: Software product line engineering enables proactive reuse among a set of related products through explicit modeling of commonalities and differences among them. Software product lines are intended to be used in a long period of time. As a result, they evolve over time, due to the changes in the requirements. Having several individual products in a software family, verification of the entire family may take a considerable effort. In this paper we aim to decrease this cost by reducing the number of verified products using static analysis techniques. Furthermore, to reduce model checking costs after product line evolution, we restrict the number of products that should be re-verified by reusing the previous verification result. All proposed techniques are based on static analysis of the product family model with respect to the property and can be automated. To show the effectiveness of these techniques we apply them on a set of case studies and present the results. [Copyright &y& Elsevier]

Ensuring the correctness of a given software component has become a crucial aspect in software engineering and model checking provides an almost fully automatic way of achieving this goal. Due to the scalability problems of the model checking technique, it has become popular to apply it at early stages in the development process, when the size of the model is much smaller than the final code. Properties proved in this way can be shown to hold at the implementation level provided that the final code refines the original specification. In this paper we focus on the main issues for adding model checking functionality to the RAISE specification language (RSL) and present the semantic foundations of our current approach for doing so. We also describe a way to use model checking to verify RAISE confidence conditions, ensuring the soundness and completeness of the results checked in this way. We then present the most interesting details of the implementation of a tool that follows the described approach. Finally, we illustrate the application of the technique with two case studies: a Digital Multiplexed Radio Telephone System and the Mondex electronic purse. [ABSTRACT FROM AUTHOR]

Abstract: This paper explains how the Spin model checker can be used to guide and inform the development of more reliable Intelligent Environments. The idea is to present a methodological guide which provides strategies and suggestions on how to model, simulate and verify these types of systems, as well as to facilitate the use of well-known tools like Spin in the development of Intelligent Environments. These tools, which have been developed by the Software Engineering community, have proven their usefulness for improving the quality of complex software systems, even in the industry field. However, researchers and developers in the area of Intelligent Environments do not usually make use of these tools. Our aim is therefore to encourage their use by colleagues working in this area to increase the reliability of these complex systems, which integrate aspects and elements of networks, sensors/actuators, ubiquitous/pervasive computing, human–computer interaction and artificial intelligence, among other related areas. [Copyright &y& Elsevier]

The paradigm of service-oriented computing revolutionized the field of software engineering. According to this paradigm, new systems are composed of existing stand-alone services to support complex cross-organizational business processes. Correct communication of these services is not possible without a proper coordination mechanism. The Reo coordination language is a channel-based modeling language that introduces various types of channels and their composition rules. By composing Reo channels, one can specify Reo connectors that realize arbitrary complex behavioral protocols. Several formalisms have been introduced to give semantics to Reo. In their most basic form, they reflect service synchronization and dataflow constraints imposed by connectors. To ensure that the composed system behaves as intended, we need a wide range of automated verification tools to assist service composition designers. In this paper, we present our framework for the verification of Reo using the $${{\tt mCRL2}}$$ toolset. We unify our previous work on mapping various semantic models for Reo, namely, constraint automata, timed constraint automata, coloring semantics and the newly developed action constraint automata, to the process algebraic specification language of $${{\tt mCRL2}}$$, address the correctness of this mapping, discuss tool support, and present a detailed example that illustrates the use of Reo empowered with $${{\tt mCRL2}}$$ for the analysis of dataflow in service-based process models. [ABSTRACT FROM AUTHOR]

Abstract: Software systems assembled from a large number of autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL (Chaki et al. (2004, 2005) ) incorporates both states and events to express important properties of component-based software systems. The main contribution of this paper is a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence. To bring some evidence of the method’s efficiency, we present some of the results obtained by employing the partial order reduction technique within our tool for verification of component-based systems modelled using the formalism of component-interaction automata (Brim et al. (2005) ). [Copyright &y& Elsevier]

Abstract: Service-Oriented Architectures (SOAs) provide methods and technologies for modelling, programming and deploying software applications that can run over globally available network infrastructures. Current software engineering technologies for SOAs, however, remain at the descriptive level and lack rigorous foundations enabling formal analysis of service-oriented models and software. To support automated verification of service properties by relying on mathematically founded techniques, we have developed a software tool that we called Venus (Verification ENvironment for UML models of Services). Our tool takes as an input service models specified by UML 2.0 activity diagrams according to the UML4SOA profile, while its theoretical bases are the process calculus COWS and the temporal logic SocL. A key feature of Venus is that it provides access to verification functionalities also to those users not familiar with formal methods. Indeed, the tool works by first automatically translating UML4SOA models and natural language statements of service properties into, respectively, COWS terms and SocL formulae, and then by automatically model checking the formulae over the COWS terms. In this paper we present the tool, its architecture and its enabling technologies by also illustrating the verification of a classical ‘travel agency’ scenario. [ABSTRACT FROM AUTHOR]

Abstract: Despite diligent efforts made by the software engineering community, the failure of software projects keeps increasing at an alarming rate. After two decades of this problem reoccurring, one of the leading causes for the high failure rate is still poor process modeling (requirements’ specification). Therefore both researchers and practitioners recognize the importance of business process modeling in understanding and designing accurate software systems. However, lack of direct model checking (verification) feature is one of the main shortcomings in conventional process modeling methods. It is important that models provide verifiable insight into underlying business processes in order to design complex software systems such as Enterprise Information Systems (EIS). The software engineering community has been deploying the same methods that have haunted the industry with failure. In this paper, we try to remedy this issue by looking at a non-conventional framework. We introduce a business process modeling method that is amenable to automatic analysis (simulation), yet powerful enough to capture the rich reality of business systems as enacted in the behavior and interactions of users. The proposed method is based on the innovative language-action perspective. [Copyright &y& Elsevier]

In the past, logics of several kinds have been proposed for reasoning about discrete-time or continuous-time Markov chains. Most of these Logics rely on either state labels (atomic propositions) or on transition labels (actions). However, in several applications it is useful to reason about both state properties and action sequences. For this purpose, we introduce the logic asCSL which provides a powerful means to characterize execution paths of Markov chains with actions and state labels asCSL can be regarded as an extension of the purely state-based logic CSL (continuous stochastic logic) In asCSL path properties are characterized by regular expressions over actions and state formulas. Thus, the truth value of path formulas depends not only on the available actions in a given time interval, but also on the validity of certain state formulas in intermediate states. We compare the expressive power of CSL and asCSL and show that even the state-based fragment of asCSL is strictly more expressive than CSL if time intervals starting at zero are employed. Using an automaton-based technique, an asCSL formula and a Markov chain with actions and state labels are combined into a product Markov chain. For time intervals starting at zero, we establish a reduction of the model checking problem for asCSL to CSL model checking on this product Markov chain. The usefulness of our approach is illustrated with an elaborate model of a scalable cellular communication system, for which several properties are formalized by means of asCSL formulas and checked using the new procedure. [ABSTRACT FROM AUTHOR]