This paper presents a technique for using execution traces to mine parametric temporal specifications in the form of quantified event automata (QEA) - previously introduced as an expressive and efficient formalism for runtime verification. We consider a pattern-based mining approach that uses a pattern library to generate and check potential properties over given traces, and then combines successful patterns. By using predefined models to measure the tool's precision and recall we demonstrate that our approach can effectively and efficiently extract specifications in realistic scenarios.

In Barringer et al. (2004,Vol. 2937, LNCS), Eagle was introduced as a general purpose rule-based temporal logic for specifying run-time monitors. A novel interpretative trace-checking scheme via stepwise transformation of an Eagle monitoring formula was defined and implemented. However, even though Eagle presents an elegant formalism for the expression of complex trace properties, Eagle's interpretation scheme is complex and appears difficult to implement efficiently. In this article, we introduce RuleR, a primitive conditional rule-based system, which has a simple and easily implemented algorithm for effective run-time checking, and into which one can compile a wide range of temporal logics and other specification formalisms used for run-time verification. As a formal demonstration, we provide a translation scheme for linear-time propositional temporal logic with a proof of translation correctness. We then introduce a parameterized version of RuleR, in which rule names may have rule-expression or data parameters, which then coincides with the same expressivity as Eagle with data arguments. RuleR with just rule-expression parameters extend the expressiveness of RuleR strictly beyond the class of context-free languages. For the language classes expressible in propositional RuleR, the addition of rule-expression and data parameters enables more compact translations. Finally, we outline a few simple syntactic extensions of ‘core’ RuleR that can lead to further conciseness of specification but still enabling easy and efficient implementation.

Cyber-physical systems denote a new modeling paradigm that promotes a holistic view on complex systems. These systems have been studied before from various particular perspectives using paradigms like ubiquitous and distributed computing or embedded and hybrid systems. In modeling cyber-physical systems one has to consider the interaction between physics, computation and communication (networking), and a formal framework to study this systems has to be invented. In this paper we develop a formal approach called Hilbertean formal methods to provide a denotational semantics for cyber-physical systems. We combine denotational semantics with an algebraic model for physical processes to model physical causality and observability.

Achieving privacy preservation in a data-sharing computing environment is a challenging problem. The requirements for a privacy preserving data access policy should be formally specified in order to be able to establish consistency between the privacy policy and its purported implementation in practice. Previous work has shown that when specifying a privacy policy, the notion of purpose should be used as the basis for access control. A privacy policy should ensure that data can only be used for its intended purpose, and the access purpose should be compliant with the data's intended purpose. This paper presents a mechanism to specify privacy policy using VDM. The entities in the purpose-based access control model are specified, the invariants corresponding to the privacy requirements in privacy policy are specified, and the operations in the model and their proof obligations are defined and investigated.

We present a revision-based logical framework for modelling hierarchical assemblies of evolvable component systems. An evolvable component is a tight coupling of a pair of components, consisting of a supervisor and a supervisee, with the supervisor able to both monitor and evolve its supervisee. An evolvable component pair is itself a component so may have its own supervisor, or may be encapsulated as part of a larger component. Components are modelled as logical theories containing actions which describe state revisions. Supervisor components are modelled as theories which are logically at a meta-level to their supervisee. Revision actions at the meta-level describe theory changes in the supervisee at the object-level. These correspond to various evolutionary changes in the component. We present this framework and show how it enables us to describe the architecture and logical structure of evolvable systems.

Summary form only given. We briefly present a rule-based framework, called EAGLE, shown to be capable of defining and implementing finite trace monitoring logics, including future and past time temporal logic, extended regular expressions, real-time and metric temporal logics (MTL), interval logics, forms of quantified temporal logics, and so on. In this paper we focus on a linear temporal logic (LTL) specialisation of EAGLE. For an initial formula of size m, we establish upper bounds of O(m/sup 2/2/sup m/logm) and O(m/sup 4/2/sup 2m/log/sup 2/m) for the space and time complexity, respectively, of single step evaluation over an input trace. EAGLE has been successfully used, in both LTL and metric LTL forms, to test a real-time controller of an experimental NASA planetary rover.

Model checking is an automated technique that can be used to determine whether a system satisfies certain required properties. The typical approach to verifying properties of software components is to check them for all possible environments. In reality, however, a component is only required to satisfy properties in specific environments. Unless these environments are formally characterized and used during verification (assume-guarantee paradigm), the results returned by verification can be overly pessimistic. This work defines a framework that brings a new dimension to model checking of software components. When checking a component against a property, our model checking algorithms return one of the following three results: the component satisfies a property for any environment; the component violates the property for any environment; or finally, our algorithms generate an assumption that characterizes exactly those environments in which the component satisfies its required property. Our approach has been implemented in the LTSA tool and has been applied to the analysis of a NASA application.

Recently, there has been considerable interest in asynchronous design techniques, particularly at the chip level. New compositional approaches, such as Sutherland's micropipeline design philosophy, have greatly assisted development. However, sophisticated CAD systems for such specialized asynchronous systems are not yet widely available, hampering the development of asynchronous design. The Rainbow asynchronous design framework is based upon a high-level multi-view design representation for micropipelines. The system contains a collection of formally based design representation and support tools. The Green sub-language supports textual/schematic static dataflow descriptions. Yellow is an imperative, control-flow parallel language, with an Ada-like rendezvous. Tables allow concise definition of combined functional and dataflow control blocks. The sub-languages have common sets of data expressions, functions and types. The formal semantics for the Rainbow sub-languages is defined via a specialized process term language called APA, producing a compact, direct semantic representation with little unnecessary encoding. APA has micropipeline primitives, uses rich structured actions and anextended Ada-like rendezvous as its atomic communication. These features enable the semantics to be defined at a suitable high level of abstraction, i.e. micropipelines. The semantic representation acts as a basis for formal analysis tools, with the aim of extending their tractability. The Rainbow design system contains textual and graphical editors for design entry, and compilation and simulation tools, supporting animation of schematics. State generation tools provide an interface to external formal analysis systems. Rainbow currently incorporates a novel on-the-fly CTL* model checker. The MARBLE asynchronous bus design from the AMULET3 microprocessor is used as an example.

A process algebraic foundation has been developed for formal analysis of synchronous hardware designs represented through the commercially available hardware design language, ELLA. An underlying semantic foundation, based on input/output trace sets, is presented first through the use of state machines. Such a representation enables direct application of standard, fully automated trace equivalence checking tools. However, to overcome the computational limitations imposed by such analysis methods, the input/output trace semantics is represented through a synchronous process algebra, EPA. Primitive processes in EPA denote the behaviour of primitive hardware components, such as delays or multiplexers, with composition operators corresponding to the different ways in which behaviours may be built. Of particular significance is the parallel composition operator which captures the machinery for building networks from other components/networks. Actions in EPA are structured and signify the state of input and output signals. This structure, however, is abstracted by developing an algebra for the actions. In particular, parallel composition on processes neatly lifts to a special (synchronous) product operation on actions. The EPA representation forms a good basis for semi-automated high-level symbolic manipulation and reasoning tools. First, the original design structure can be maintained, thus easing the problems of user level feedback from tools. Secondly, the application of EPA to ELLA enables a deterministic finite automation form for EPA terms. This provides a route to tractable symbolic verification and simulation, using a state evolution method to establish strong bisimulation properties. The method has been successfully applied to classes of unbounded state space systems.

Abstract In this paper a methodology for the use of temporal logic as an executable imperative language is introduced. The approach, which provides a concrete framework, calledMetateM, for executing temporal formulae, is motivated and illustrated through examples. In addition, this introduction provides references to further, more detailed, work relating to theMetateMapproach to executable logics.

Editorial Get access HOWARD BARRINGER HOWARD BARRINGER Executive Editor Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 1, Issue 5, October 1991, Pages 573–574, https://doi.org/10.1093/logcom/1.5.573 Published: 01 October 1991

A formal specification of a multiple-life system is constructed. The example illustrates and justifies one of many possible system specification styles based on temporal techniques.

In this paper we advance the radical notion that a computational model based on the reals provides a more abstract description of concurrent and reactive systems, than the conventional integers based behavioral model of execution sequences. The real model is studied in the setting of temporal logic, and we illustrate its advantages by providing a fully abstract temporal semantics for a simple concurrent language, and an example of verification of a concurrent program within the real temporal logic defined here. It is shown that, by imposing the crucial condition of finite variability, we achieve a balanced formalism that is insensitive to finite stuttering, but can recognize infinite stuttering, a distinction which is essential for obtaining a fully abstract semantics of non-terminating processes. Among other advantages, going into real-based semantics obviates the need for the controversial representation of concurrency by interleaving, and most of the associated fairness constraints.

An axiomatic proof system for reasoning about the basic Ada tasking constructs is presented. The proof system is based on an earlier paper by the same authors and deals with safety properties of concurrent Ada programs including freedom from deadlock. The system has been proved to be sound and relatively complete against a denotational semantics for the constructs considered.

A compositional temporal logic proof system for the specification and verification of concurrent programs is presented. Versions of the system are developed for shared variables and communication based programming languages that include procedures.

Abstract Portability of MUSS compilers is achieved by using an abstract machine model concept. Two different abstract models, both suited for multi‐language multi‐machine usage, have been developed and evaluated. These models differ mainly in the level of interface to the compiler. The form of these models and the performance of two compilers, each using both models, are presented.