Experimental evaluation of a tool for the verification and transformation of source code in event-driven systems

In event-driven systems, separating the reactive part of software (i.e., event-driven control) from the non-reactive part is a common design practice. The reactive part is typically structured according to the states and transitions of a system, whereas the non-reactive part is typically structured according to the concepts of the application domain (e.g., the services provided by the system). In such systems, the non-reactive part of software stimulates the reactive part with event calls. Whenever the non-reactive part is modified (e.g., during evolution), the existing event calls may become invalid, new event calls may become necessary, and the two parts of software may become incompatible. Manually finding and repairing these types of defects is a time-consuming and error-prone maintenance task. In this article, we present a solution that combines source code model checking and aspect-oriented programming techniques, to reduce the time spent by developers and to automatically find defects, while performing the maintenance task mentioned above. In addition, we present controlled experiments showing that the solution can reduce the time by 75%, and enable the prevention of one defect per 140 lines of source code.     

Predicate diagrams for the verification of real-time systems

This article discusses a new format of predicate diagrams for the verification of real-time systems. We consider systems that are defined as extended timed graphs, a format that combines timed automata and constructs for modelling data, possibly over infinite domains. Predicate diagrams are succinct and intuitive representations of Boolean abstractions. They also represent an interface between deductive tools used to establish the correctness of an abstraction, and model checking tools that can verify behavioral properties of finite-state models. The contribution of this article is to extend the format of predicate diagrams to timed systems. We establish a set of verification conditions that are sufficient to prove that a given predicate diagram is a correct abstraction of an extended timed graph; these verification conditions can often be discharged with SMT solvers such as CVC-lite. Additionally, we describe how this approach extends naturally to the verification of parameterized systems. The formalism is supported by a toolkit, and we demonstrate its use at the hand of Fischer’s real-time mutual-exclusion protocol.     

Runtime verification of embedded real-time systems

We present a runtime verification framework that allows on-line monitoring of past-time Metric Temporal Logic (ptMTL) specifications in a discrete time setting. We design observer algorithms for the time-bounded modalities of ptMTL, which take advantage of the highly parallel nature of hardware designs. The algorithms can be translated into efficient hardware blocks, which are designed for reconfigurability, thus, facilitate applications of the framework in both a prototyping and a post-deployment phase of embedded real-time systems. We provide formal correctness proofs for all presented observer algorithms and analyze their time and space complexity. For example, for the most general operator considered, the time-bounded Since operator, we obtain a time complexity that is doubly logarithmic both in the point in time the operator is executed and the operator’s time bounds. This result is promising with respect to a self-contained, non-interfering monitoring approach that evaluates real-time specifications in parallel to the system-under-test. We implement our framework on a Field Programmable Gate Array platform and use extensive simulation and logic synthesis runs to assess the benefits of the approach in terms of resource usage and operating frequency.     

An engineering process for the verification of real-time systems

The complete verification of the timing properties of a large critical system cannot be undertaken in a single step or with a single method. In this paper we present a process that links together a number of techniques and approaches that cover all stages of development from requirements analysis to code testing. The key elements of the process are: a constrained form of timed automata that uses delay and deadline to define temporal behaviour, notions of rely and guarantee to cover temporal dependencies, model checking for design verification, SPARK and Ravenscar restrictions for programming, and scheduling and response time analysis for asserting implementation compliance. Extended examples of the use of the process are given.     

Object-oriented specification and formal verification of real-time systems

An object-oriented approach for specification and verification of real-time systems is described in this paper. It is motivated by taking advantage of object-oriented techniques to produce real-time software that is easy to understand, maintain, and reuse. The approach specifies the structural, behavioral, and control aspects of objects in one model with a textual representation as well as a graphical representation. For ease to comprehend and use, the model encapsulates object states and allows an analyst to focus on specifying object operations one at a time. System behavior from individual objects can be deduced and analyzed. For safety considerations, the approach supports specification of failures to object behavior and their resultant faults. The approach also supports modeling of timed temporal constraints for specifying and verifying desirable real-time properties. An object timed temporal logic OTTL is defined for expressing the syntax and semantics of these constraints. Decision procedures for their verification are also presented.     

Compositional verification of real-time systems using Ecdar

We present a specification theory for timed systems implemented in the Ecdar tool. We illustrate the operations of the specification theory on a running example, showing the models and verification checks. To demonstrate the power of the compositional verification, we perform an in depth case study of a leader election protocol; Modeling it in Ecdar as Timed input/output automata Specifications and performing both monolithic and compositional verification of two interesting properties on it. We compare the execution time of the compositional to the classical verification showing a huge difference in favor of compositional verification.     

Scenario-based verification of real-time systems using Uppaal

This article proposes two approaches to tool-supported automatic verification of dense real-time systems against scenario-based requirements, where a system is modeled as a network of timed automata (TAs) or as a set of driving live sequence charts (LSCs), and a requirement is specified as a separate monitored LSC chart. We make timed extensions to a kernel subset of the LSC language and define a trace-based semantics. By translating a monitored LSC chart to a behavior-equivalent observer TA and then non-intrusively composing this observer with the original TA-modeled real-time system, the problems of scenario-based verification reduce to computation tree logic (CTL) real-time model checking problems. When the real-time system is modeled as a set of driving LSC charts, we translate these driving charts and the monitored chart into a behavior-equivalent network of TAs by using a “one-TA-per-instance line” approach, and then reduce the problems of scenario-based verification also to CTL real-time model checking problems. We show how we exploit the expressivity of the TA formalism and the CTL query language of the real-time model checker Uppaal to accomplish these tasks. The proposed two approaches are implemented in the Uppaal tool and built as a tool chain, respectively. We carry out a number of experiments with both verification approaches, and the results indicate that these methods are viable, computationally feasible, and the tools are effective.     

Behavioral modeling and verification of multi-agent systems for manufacturing control

Simulation is the primary approach to the performance analysis of multi-agent manufacturing systems. In a typical simulation experiment, varying the agent negotiation protocol’s timing parameters can yield incomparable results in performance terms due to behavioral problems such as deadlocks and livelocks. Formal verification can help resolve such problems and therefore plays an important role in the design of agent negotiation protocols. We describe an efficient and scalable approach to formal verification based on an industrial-strength model checking tool and illustrate it with an example.     

PREPARE: a tool for knowledge base verification

The knowledge base is the most important component in a knowledge-based system. Because a knowledge base is often built in an incremental, piecemeal fashion, potential errors may be inadvertently brought into it. One of the critical issues in developing reliable knowledge-based systems is how to verify the correctness of a knowledge base. The paper describes an automated tool called PREPARE for detecting potential errors in a knowledge base. PREPARE is based on modeling a knowledge base by using a predicate/transition net representation. Inconsistent, redundant, subsumed, circular, and incomplete rules in a knowledge base are then defined as patterns of the predicate/transition net model, and are detected through a syntactic pattern recognition method. The research results to date have indicated that: the methodology ran be adopted in knowledge-based systems where logic is used as knowledge representation formalism; the tool can be invoked at any stage of the system's development, even without a fully functioning inference engine; the predicate/transition net model of knowledge bases is easy to implement and provides a clear and understandable display of the knowledge to be used by the system     

A methodology for design, test, and evaluation of real-time systems

This article presents a methodology that is suitable for use as part of either a prototyping approach or a component-reuse approach. This methodology integrates modeling and simulation as well as developmental and operational testing over the life cycle. The type of systems or components we address operate in real time. Designing and testing real-time systems involves the use of multiple processors and communication links. The real-time system itself can run on a single processor or multiple processors. Even when the system runs on a single processor, the test and evaluation environment uses multiple processors. If the evaluation environment were hosted on the system processor, system performance would be affected. For ease of exposition, we focus on sensor systems; the methodology described is widely applicable to other kinds of systems. We use two examples (a space-borne navigation system and an interferometer system) to describe the methodology and show how it can be used. This methodology can reduce project costs and shorten schedules because it requires performance evaluation and integration testing early, when problems are generally easier and less costly to correct     

Modeling and verification of real-time embedded systems with urgency

Real-time embedded systems are often designed with different types of urgencies such as delayable or eager, that are modeled by several urgency variants of the timed automata model. However, most model checkers do not support such urgency semantics, except for the IF toolset that model checks timed automata with urgency against observers. This work proposes an Urgent Timed Automata (UTA) model with zone-based urgency semantics that gives the same model checking results as absolute urgency semantics of other existing urgency variants of the timed automata model, including timed automata with deadlines and timed automata with urgent transitions. A necessary and sufficient condition, called complete urgency, is formulated and proved for avoiding zone partitioning so that the system state graphs are simpler and model checking is faster. A novel zone capping method is proposed that is time-reactive, preserves complete urgency, satisfies all deadlines, and does not need zone partitioning. The proposed verification methods were implemented in the SGM CTL model checker and applied to real-time and embedded systems. Several experiments, comparing the state space sizes produced by SGM with that by the IF toolset, show that SGM produces much smaller state-spaces.     

An iterative approach to verification of real-time systems

Verification of real-time systems is a complex problem, requiring construction of aregion automaton with a state space growing exponentially in the number of timing constraints and the sizes of constants in those constraints. However, some properties can be verified even when some quantitative timing information is abstracted. We propose a new verification procedure, where increasingly more complex abstractions of the region automaton are iteratively constructed. In many cases, the procedure can be stopped early, and thus can avoid the state space explosion problem.     

Model and algorithm for efficient verification of high-assurance properties of real-time systems

In this paper, we present a new compositional verification methodology for efficiently verifying high-assurance properties such as reachability and deadlock freedom of real-time systems. In this methodology, each component of real-time systems is initially specified as a timed automaton and it communicates with other components via synchronous and/or asynchronous communication channels. Then, each component is analyzed by a generation of its state-space graph which is formalized as a new state-space representation model called Multiset Labeled Transition Systems (MLTSs). Afterward, the state spaces of the components are hierarchically composed and simplified through a composition algorithm and a set of condensation rules, respectively, to get a condensed state space of the system. The simplified state spaces preserve equivalence with respect to deadlock and reachable states. Such equivalence is assured by our reduction theories called IOT-failure equivalence and IOT-state equivalence. To show the performance of our methodology, we developed a verification tool RT-IOTA and carried out experiments on some benchmarks such as CSMA/CD protocol, a rail-road crossing, an alternating bit-protocol, etc. Specifically, we look at the time taken to generate the statespace, the size of the state space, and the amount of reduction achieved by our condensation rules. The results demonstrate the strength of our new technique in dealing with the state-explosion problem.     

Towards modeling and runtime verification of self-organizing systems

According to the fact that the intrinsic dynamism of self-organizing systems challenges the existing methods of engineering for modeling reliable complex systems, in this paper, we propose a new formal-based method to model self-organizing systems. The capabilities of the proposed method which are used to address several challenges in design, development and analysis of self-organizing systems are: modularity and robustness, decentralized control and scalability, required adaptation types, flexible and adaptive control mechanism, separation of adaptation and business logic, and safe adaptation. To evaluate the proposed method, we use self-organizing traffic management system as a case study and exploit the proposed method for modeling this dynamic system. Moreover, we propose and employ a novel policy-based runtime verification mechanism to ensure that the safety properties are satisfied by the implementation at runtime. We provide our case study prototype using Java and the Ponder2 toolkit and apply our runtime verification method to show its proper reaction capabilities to the property violations. This benefit is the result of using dynamic policies in our method to control the behavior of systems.     

A generic framework for modeling heterogeneous real-time systems

Complex real-time systems usually consist of heterogeneous components. These components interact with different semantics. Modeling these systems normally need integrating several domain-specific tools such as UML, Simulink. But interchanging data between these tools is very difficult. UML is a standard modeling language for object-oriented software development, used more and more in real-time domain. It provides several extensibility mechanisms to allow modeling special domains. This paper presents a generic framework, which is based on UML notations and metamodels, for heterogeneous modeling real-time systems. So engineers from different domains can work together on a unified platform.     

Scenario-based requirements analysis techniques for real-time software systems: a comparative evaluation

One of the most critical phases of software engineering is requirements elicitation and analysis. Success in a software project is influenced by the quality of requirements and their associated analysis since their outputs contribute to higher level design and verification decisions. Real-time software systems are event driven and contain temporal and resource limitation constraints. Natural-language-based specification and analysis of such systems are then limited to identifying functional and non-functional elements only. In order to design an architecture, or to be able to test and verify these systems, a comprehensive understanding of dependencies, concurrency, response times, and resource usage are necessary. Scenario-based analysis techniques provide a way to decompose requirements to understand the said attributes of real-time systems. However they are in themselves inadequate for providing support for all real-time attributes. This paper discusses and evaluates the suitability of certain scenario-based models in a real-time software environment and then proposes an approach, called timed automata, that constructs a formalised view of scenarios that generate timed specifications. This approach represents the operational view of scenarios with the support of a formal representation that is needed for real-time systems. Our results indicate that models with notations and semantic support for representing temporal and resource usage of scenario provide a better analysis domain.H. Saiedian is a member of the Information & Telecommunication Technology Center at the University of Kansas. His research was partially supported by a grant from the National Science Foundation (NSF).     

An object-oriented tool for simulating distributed real-time control systems

This paper presents an object-oriented software tool, called RTSIM, aimed at simulating real-time embedded controllers. The tool consists of a collection of C++ libraries permitting a separate specification of the functional behaviour of the controller and of the hardware/software architecture to be used for its deployment. In particular, it is possible to provide an accurate modelling of the concurrent architecture of the control tasks and of the run-time support offered by the operating system for the real-time scheduling of the shared resources (CPU, memory buffers and network links). In this way, it is possible to compare different scheduling solutions by evaluating their simulated performance directly in the domain of the control application. Moreover, the tool can be utilized to tune up design parameters such as the activation frequencies of the tasks. The application of the tool is shown in a meaningful case study. Copyright © 2002 John Wiley & Sons, Ltd.