Extending statecharts with temporal logic

The task of designing large real-time reactive systems, which interact continuously with their environment and exhibit concurrency properties, is a challenging one. The authors explore the utility of a combination of behavior and function specification languages in specifying such systems and verifying their properties. An existing specification language, statecharts, is used to specify the behavior of real-time reactive systems, while a new logic-based language called FNLOG (based on first-order predicate calculus and temporal logic) is designed to express the system functions over real time. Two types of system properties, intrinsic and structural, are proposed. It is shown that both types of system properties are expressible in FNLOG and may be verified by logical deduction, and also hold for the corresponding behavior specification     

Timed Automata Patterns

Timed Automata have proven to be useful for specification and verification of real-time systems. System design using Timed Automata relies on explicit manipulation of clock variables. A number of automated analyzers for Timed Automata have been developed. However, Timed Automata lack of composable patterns for high-level system design. Logic-based specification languages like Timed CSP and TCOZ are well suited for presenting compositional models of complex real-time systems. In this work, we define a set of composable Timed Automata patterns based on hierarchical constructs in timed enriched process algebras. The patterns facilitate hierarchical design of complex systems using Timed Automata. They also allow a systematic translation from Timed CSP/TCOZ models to Timed Automata so that analyzers for Timed Automata can be used to reason about TCOZ models. A prototype has been developed to support system design using Timed Automata patterns or, if given a TCOZ specification, to automate the translation from TCOZ to Timed Automata.     

Semantic properties of Lucid's compute clause and its compilation

Compilation algorithms for a subset of the programming language Lucid are extended so that programs with nested compute clauses can be compiled.The extension is derived from the semantic properties of the compute clause construct, and is applicable to a broad class of compilation algorithms for a subset of Lucid. A correctness proof of the extension is also given.This work has been supported in part by an NSF grant MCS 78-01812     

Requirements specification of real-time systems: temporal parameters and timing-constraints

The development of high-quality real-time systems depends on their correct requirements specification, which includes the analysis and specification of timing issues. This paper focuses on requirements specification of real-time systems, presenting a set of temporal parameters and timing-constraints related to the execution of systems processes. Timing-constraints are expressed by formulas, being useful for defining, representing, and validating the system temporal behavior, particularly in hard real-time systems specifications. The primary contribution over previous studies is the proposal of a more generic and complete set of timing-constraints, applied to the area of requirements engineering for real-time systems, which has not been sufficiently explored.     

Specification and analysis of real-time systems with PARAGON

This paper describes a methodology for the specification and analysis of distributed real-time systems using the toolset called PARAGON. PARAGON is based on the Communicating Shared Resources paradigm, which allows a real-time system to be modeled as a set of communicating processes that compete for shared resources. PARAGON supports both visual and textual languages for describing real-time systems. It offers automatic analysis based on state space exploration as well as user-directed simulation. Our experience with using PARAGON in several case studies resulted in a methodology that includes design patterns and abstraction heuristics, as well as an overall process. This paper briefly overviews the communicating shared resource paradigm and its toolset PARAGON, including the textual and visual specification languages. The paper then describes our methodology with special emphasis on heuristics that can be used in PARAGON to reduce the state space. To illustrate the methodology, we use examples from a real-life system case study. This revised version was published online in June 2006 with corrections to the Cover Date.     

An interval logic for real-time system specification

Formal techniques for the specification of real time systems must be capable of describing system behavior as a set of relationships expressing the temporal constraints among events and actions, including properties of invariance, precedence, periodicity, liveness, and safety conditions. The paper describes a Temporal-Interval Logic with Compositional Operators (TILCO) designed expressly for the specification of real time systems. TILCO is a generalization of classical temporal logics based on the operators, eventually and henceforth; it allows both qualitative and quantitative specification of time relationships. TILCO is based on time intervals and can concisely express temporal constraints with time bounds, such as those needed to specify real time systems. This approach can be used to verify the completeness and consistency of specifications, as well as to validate system behavior against its requirements and general properties. TILCO has been formalized by using the theorem prover Isabelle/HOL. TILCO specifications satisfying certain properties are executable by using a modified version of the Tableaux algorithm. The paper defines TILCO and its axiomatization, highlights the tools available for proving properties of specifications and for their execution, and provides an example of system specification and validation     

The Real-Time Process Algebra (RTPA)

The real-time process algebra (RTPA) is a set of new mathematical notations for formally describing system architectures, and static and dynamic behaviors. It is recognized that the specification of software behaviors is a three-dimensional problem known as: (i) mathematical operations, (ii) event/process timing, and (iii) memory manipulations. Conventional formal methods in software engineering were designed to describe the 1-D (type (i)) or 2-D (types (i) and (iii)) static behaviors of software systems via logic, set and type theories. However, they are inadequate to address the 3-D problems in real-time systems. A new notation system that is capable to describe and specify the 3-D real-time behaviors, the real-time process algebra (RTPA), is developed in this paper to meet the fundamental requirements in software engineering.RTPA is designed as a coherent software engineering notation system and a formal engineering method for addressing the 3-D problems in software system specification, refinement, and implementation, particularly for real-time and embedded systems. In this paper, the RTPA meta-processes, algebraic relations, system architectural notations, and a set of fundamental primary and abstract data types are described. On the basis of the RTPA notations, a system specification method and a refinement scheme of RTPA are developed. Then, a case study on a telephone switching system is provided, which demonstrates the expressive power of RTPA on formal specification of both software system architectures and behaviors. RTPA elicits and models 32 algebraic notations, which are the common core of existing formal methods and modern programming languages. The extremely small set of formal notations has been proven sufficient for modeling and specifying real-time systems, their architecture, and static/dynamic behaviors in real-world software engineering environment.     

Specification and analysis of parallel/distributed software andsystems by Petri nets with transition enabling functions

An approach for visually specifying parallel/distributed software using Petri nets (PNs) extend with transition enabling functions (TEFs) is investigated. The approach is demonstrated to be useful in the specification of decision-making activities that control distributed computing systems. PNs are employed because of their highly visual nature that can give insight into the nature of the controller of such a system and because of their analytical properties. In order to increase the expressive power of PNs, the extension of TEFs is used. The main focus is the specification and analysis of parallel/distributed software and systems. A key element of this approach is a set of rules derived to automatically transform such an extended net into a basic PN. Once the rules have been applied to transform the specification, analytical methods can be used to investigate characteristic properties of the system and validate correct operation     

Modechart: a specification language for real-time systems

Present a specification language for real-time systems called Modechart. The semantics of Modechart is given in terms of real-time logic (RTL), which is especially amenable to reasoning about the absolute (real-time clock) timing of events. The semantics of Modechart has an important property that the translation of a Modechart specification into RTL formulas results in a hierarchical organization of the resulting RTL assertions. This gives us significant leverage in reasoning about properties of a system by allowing us to filter out assertions that concern lower levels of abstraction. Some results about desirable properties of Modechart specifications are given. A graphical implementation of Modechart has been completed     

A Complete Axiomatization of Finite-state ACSR Processes

A real-time process algebra, called ACSR, has been developed to facilitate the specification and analysis of real-time systems. ACSR supports synchronous timed actions and asynchronous instantaneous events. Timed actions are used to represent the usage of resources and to model the passage of time. Events are used to capture synchronization between processes. To be able to specify real-time systems accurately, ACSR supports a notion of priority that can be used to arbitrate among timed actions competing for the use of resources and among events that are ready for synchronization. In addition to operators common to process algebra, ACSR includes the scope operator, which can be used to model timeouts and interrupts. Equivalence between ACSR terms is based on the notion of strong bisimulation. This paper briefly describes the syntax and semantics of ACSR and then presents a set of algebraic laws that can be used to prove equivalence of ACSR processes. The contribution of this paper is the soundness and completeness proofs of this set of laws. The completeness proof is for finite-state ACSR processes, which are defined to be processes without free variables under parallel operator or scope operator.     

Invariants in the application-oriented specification of control systems

The importance of an application-oriented specification as the starting point for control system design has recently been recognized. As an initial stage of the work of a Special Interest Group on Application Oriented Specifications, Halling and others presented a review of the problem and some of the approaches to specification in current use. Control applications were divided into two broad classes: continuous control systems on the one hand, and sequential or discrete variable control systems on the other. Within the class of discrete systems a subclass of systems, where large volumes of data must be handled and real-time data manipulations must be specified, was also recognized. This paper aims to show that emphasis on the invariant properties of system elements can be helpful in presenting a system specification for all these types of systems.     

Towards a denotational semantics of timed RSL using duration calculus

The Timed RAISE Specification Language(Timed RSL)is an extension of RAISE Specificatioin Language by adding time constructors for specifying real-time applications.Duration Calculus(DC) is a real-time interval logic,which can be used to specify and reason about timing and logical constraints on duration propoerties of Boolean states in a dynamic system.This paper gives a denotational semantics to a subset of Timed RSL expressions,using Duration Calculus extended with super-dense shop modality and notations to capture time point properties of piecewise continuous states of arbitrary types.Using this semantics,the paper pesents a proof rule for verifying Timed RSL iterative expressions and implements the rule to prove the satisfaction by a sample Timed RSL specification of its real-time requrements.     

Stepwise design of real-time systems

The joint action approach to modeling of reactive systems is presented and augmented with real time. This leads to a stepwise design method where temporal logic of actions can be used for formal reasoning, superposition is the key mechanism for transformations, the advantages of closed-system modularity are utilized, logical properties are addressed before real-time properties, and real-time properties are enforced without any specific assumptions on scheduling. As a result, real-time modeling is made possible already at early stages of specification, and increased insensitivity is achieved with respect to properties imposed by implementation environments     

Decentralized supervisory control of nondeterministic discrete event systems: The existence condition of a robust and nonblocking supervisor

This paper addresses a decentralized supervisory control problem for an uncertain discrete event system (DES) modeled by a set of possible nondeterministic automata with unidentified internal events. For a given language specification, we present the existence condition of a robust and nonblocking decentralized supervisor that achieves this specification for any nondeterministic model in the set. In particular, we show that the given language specification can be achieved based on the properties of its controllability and coobservability with respect to the overall nominal behavior of the uncertain DES. It is further shown that the existence of a nonblocking decentralized supervisor can be examined with a trajectory model of the language specification.     

带数据约束的概率实时系统的验证

带数据约束的概率实时系统是指一种既带有概率时间约束又带有数据变量约束的计算系统。目前将离散数据约束和连续时间约束统一在一个概率模型中的规范及验证研究较少。提出了一种既带有连续数据约束又带有离散数据约束的规范——基于连续时间的概率ZIA规范,并给出了它的时序逻辑。对于CTL和PCTL而言,尽管这些逻辑很强大,但是只能反映时序性质,因此提出一个新的形式化语言CTML来表达度量性质查询,同时保留表达时序性质的能力并给出概率ZIA规范的验证算法。     

A tool for analyzing and fine tuning the real-time properties of an embedded system

This paper describes a computer-aided software engineering (CASE) tool that helps designers analyze and fine-tune the timing properties of their embedded real-time software. Existing CASE tools focus on the software specification and design of embedded systems. However, they provide little, if any, support after the software has been implemented. Even if the developer used a CASE tool to design the system, their system most likely does not meet the specifications on the first try. This paper includes guidelines for implementing analyzable code, profiling a real-time system, filtering and extracting measured data, analyzing the data, and interactively predicting the effect of changes to the real-time system. The tool is a necessary first step towards automating the debugging and fine tuning of an embedded system's temporal properties.     

Miro: visual specification of security

Miro is a set of languages and tools that support the visual specification of file system security. Two visual languages are presented: the instance language, which allows specification of file system access, and the constraint language, which allows specification of security policies. Miro visual languages and tools are used to specify security configurations. A visual language is one whose entities are graphical, such as boxes and arrows, specifying means stating independently of any implementation the desired properties of a system. Security means file system protection: ensuring that files are protected from unauthorized access and granting privileges to some users, but not others. Tools implemented and examples of how these languages can be applied to real security specification problems are described     

用带时钟变量的线性时态逻辑扩充Object-Z*

Object-Z是形式规格说明语言Z的面向对象扩充,适合描述大型面向对象软件规格说明,但它不能很好地描述连续性实时变量和时间限制。线性时态逻辑能够描述实时系统,但不能很好地处理连续时间关系,也不能很好地模块化描述形式规格说明。首先用时钟变量扩充线性时态逻辑,接着提出了一个方法——用带时钟变量的时态逻辑(LTLC)来扩充Object-Z。用LTLC扩充的Object-Z是一个模块化规格说明语言,是Object-Z语法和语义的最小扩充,其最大优点在于它能方便地描述和验证复杂的实时软件规格说明。