Abstract Regular Tree Model Checking

Regular (tree) model checking (RMC) is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finite word or tree automata, and operations of the systems being examined as finite word or tree transducers. The reachability set is then computed by a repeated application of the transducers on the automata representing the currently known set of reachable configurations. In order to facilitate termination of RMC, various acceleration schemas have been proposed. One of them is a combination of RMC with the abstract-check-refine paradigm yielding the so-called abstract regular model checking (ARMC). ARMC has originally been proposed for word automata and transducers only and thus for dealing with systems with linear (or easily linearisable) structure. In this paper, we propose a generalisation of ARMC to the case of dealing with trees which arise naturally in a lot of modelling and verification contexts. In particular, we first propose abstractions of tree automata based on collapsing their states having an equal language of trees up to some bounded height. Then, we propose an abstraction based on collapsing states having a non-empty intersection (and thus “satisfying”) the same bottom-up tree “predicate” languages. Finally, we show on several examples that the methods we propose give us very encouraging verification results.     

Work domain analysis and sensors II: Pasteurizer II case study

In this paper we establish a foundation for understanding the instrumentation needs of complex dynamic systems if ecological interface design (EID)-based interfaces are to be robust in the face of instrumentation failures. EID-based interfaces often include configural displays which reveal the higher-order properties of complex systems. However, concerns have been expressed that such displays might be misleading when instrumentation is unreliable or unavailable. Rasmussen's abstraction hierarchy (AH) formalism can be extended to include representations of sensors near the functions or properties about which they provide information, resulting in what we call a “sensor-annotated abstraction hierarchy”. Sensor-annotated AHs help the analyst determine the impact of different instrumentation engineering policies on higher-order system information by showing how the data provided from individual sensors propagates within and across levels of abstraction in the AH. The use of sensor-annotated AHs with a configural display is illustrated with a simple water reservoir example. We argue that if EID is to be effectively employed in the design of interfaces for complex systems, then the information needs of the human operator need to be considered at the earliest stages of system development while instrumentation requirements are being formulated. In this way, Rasmussen's AH promotes a formative approach to instrumentation engineering.     

Coordination as a Service: Ontological and Formal Foundation

Coordination models like Lindawere first conceived in the context of closed systemslike high-performance parallel applications  where all coordinated entities were known once and for all at design time, and coordination media were conceptually part of a coordinated application. Correspondingly, traditional formalisations of coordination models  where both coordinated entities and coordination media are uniformly represented as terms of a process algebra  endorse the viewpoint of coordination as a language for building concurrent systems.Today, new application scenarios call for a new approach to the formalisation of coordination models and systems. The complexity of today systems requires coordination media to be seen as first-class design abstractions, affecting the engineering process down to the deployment of infrastructures providing coordination services, for which effectiveness and reliability may be critical properties demanding a formal treatment.As a unifying framework for a number of existing works on the semantics of coordination media, in this paper we present a basic ontology and a formal framework endorsing the viewpoint of coordination as a service. Typical process algebra techniques are here exploited to represent the semantics of a coordinated system in terms of the interactive behaviour of coordination media. By this framework, coordination media are seen as primary abstractions amenable of formal investigation, promoting their exploitation at any step of the engineering process.     

New results for Constraint Markov Chains

This paper studies compositional reasoning theories for stochastic systems. A specification theory combines notions of specification and implementation with satisfaction and refinement relations, and a set of operators that together support stepwise design. One of the first behavioral specification theories introduced for stochastic systems is the one of Interval Markov Chains (IMCs), which are Markov Chains whose probability distributions are replaced by a conjunction of intervals. In this paper, we show that IMCs are not closed under conjunction, which gives a formal proof of a conjecture made in several recent works.In order to leverage this problem, we suggested to work with Constraint Markov Chains (CMCs) that is another specification theory where intervals are replaced with general constraints. Contrary to IMCs, one can show that CMCs enjoy the closure properties of a specification theory. In addition, we propose aggressive abstraction procedures for CMCs. Such abstractions can be used either to combat the state-space explosion problem, or to simplify complex constraints. In particular, one can show that, under some assumptions, the behavior of any CMC can be abstracted by an IMC.Finally, we propose an algorithm for counter-example generation, in case a refinement of two CMCs does not hold. We present a tool that implements our results. Implementing CMCs is a complex process and relies on recent advances made in decision procedures for theory of reals.     

On using data abstractions for model checking refinements

In this paper we investigate how standard model checkers can be applied to checking refinement relationships between Z specifications. The major obstacle to such a use are the (potentially) infinite data domains in specifications. Consequently, we examine the application of data abstraction techniques for reducing the infinite to a finite state space. Since data abstractions do, however, decrease the amount of information in a specification, refinement can—in general—not be proven on the abstractions anymore, it can only be disproved. The model checker can thus be used to generate counter examples to a refinement relationship. Here, we show how abstract specifications can be systematically constructed (from a given data abstraction) and how a standard model checker (FDR) can be applied to find counter examples in case when refinement is absent. We especially discuss the applicability of the construction method: it constructs abstract specifications which are either upward or downward simulations of the original specifications, and depending on the operations in the specification and the data abstraction chosen, such a construction might succeed or fail. The construction abstracts both the input/output as well as the state.     

AGENT COORDINATION CONTEXTS IN A MAS COORDINATION INFRASTRUCTURE

In order to harness complexity in multi-agent systems (MAS), first-class entities that mediate interaction between agents and environment are required, which can encapsulate control over MAS behavior and evolution. To this end, MAS infrastructures should provide mediating artifacts, both enabling and constraining agent interactions, and possibly representing admissible agent perceptions and actions over the environment.

Along this line, in this paper, we take the notion of agent coordination context (ACC) as a means to model agent-environment interactions, and show how it can be embedded within a MAS infrastructure in terms of model and runtime structures. Then, we take the TuCSoN coordination infrastructure as a reference, and extend it with the ACC abstraction to integrate the support for coordination with organization and security.     

Verifying Time Partitioning in the DEOS Scheduling Kernel

This paper describes an experiment to use the Spin model checking system to support automated verification of time partitioning in the Honeywell DEOS real-time scheduling kernel. The goal of the experiment was to investigate whether model checking with minimal abstraction could be used to find a subtle implementation error that was originally discovered and fixed during the standard formal review process. The experiment involved translating a core slice of the DEOS scheduling kernel from C++ into Promela, constructing an abstract “test-driver” environment and carefully introducing several abstractions into the system to support verification. Attempted verification of several properties related to time-partitioning led to the rediscovery of the known error in the implementation. The case study indicated several limitations in existing tools to support model checking of software. The most difficult task in the original DEOS experiment was constructing an adequate environment to close the system for verification. The fidelity of the environment was of crucial importance for achieving meaningful results during model checking. In this paper, we describe the initial environment modeling effort and a follow-on experiment with using semi-automated environment generation methods. Program abstraction techniques were also critical for enabling verification of DEOS. We describe an implementation scheme for predicate abstraction, an approach based on abstract interpretation, which was developed to support DEOS verification.     

Abstraction-guided synthesis of synchronization

We present a novel framework for automatic inference of efficient synchronization in concurrent programs, a task known to be difficult and error-prone when done manually. Our framework is based on abstract interpretation and can infer synchronization for infinite state programs. Given a program, a specification, and an abstraction, we infer synchronization that avoids all (abstract) interleavings that may violate the specification, but permits as many valid interleavings as possible. Combined with abstraction refinement, our framework can be viewed as a new approach for verification where both the program and the abstraction can be modified on-the-fly during the verification process. The ability to modify the program, and not only the abstraction, allows us to remove program interleavings not only when they are known to be invalid, but also when they cannot be verified using the given abstraction. We implemented a prototype of our approach using numerical abstractions and applied it to verify several example programs.     

Automating the product derivation process of multi-agent systems product lines

Agent-oriented software engineering and software product lines are two promising software engineering techniques. Recent research work has been exploring their integration, namely multi-agent systems product lines (MAS-PLs), to promote reuse and variability management in the context of complex software systems. However, current product derivation approaches do not provide specific mechanisms to deal with MAS-PLs. This is essential because they typically encompass several concerns (e.g., trust, coordination, transaction, state persistence) that are constructed on the basis of heterogeneous technologies (e.g., object-oriented frameworks and platforms). In this paper, we propose the use of multi-level models to support the configuration knowledge specification and automatic product derivation of MAS-PLs. Our approach provides an agent-specific architecture model that uses abstractions and instantiation rules that are relevant to this application domain. In order to evaluate the feasibility and effectiveness of the proposed approach, we have implemented it as an extension of an existing product derivation tool, called GenArch. The approach has also been evaluated through the automatic instantiation of two MAS-PLs, demonstrating its potential and benefits to product derivation and configuration knowledge specification.     

Defining Database Views as Data Abstractions

The concept of data abstraction is utilized in database systems to define user interfaces via database views in database application languages and to describe the architecture of database systems. Differences between the specification and use of database views and other data abstractions realized as abstract data types are discussed. Database views are formally specified using both the algebraic specification method and the abstract model specification method. The use of database views is demonstrated via the EXT_Pascal database application language.     

PVS Strategies for Proving Abstraction Properties of Automata

Abstractions are important in specifying and proving properties of complex systems. To prove that a given automaton implements an abstract specification automaton, one must first find the correct abstraction relation between the states of the automata, and then show that this relation is preserved by all corresponding action sequences of the two automata. This paper describes tool support based on the PVS theorem prover that can help users accomplish the second task, in other words, in proving a candidate abstraction relation correct. This tool support relies on a clean and uniform technique for defining abstraction properties relating automata that uses library theories for defining abstraction relations and templates for specifying automata and abstraction theorems. The paper then describes how the templates and theories allow development of generic, high level PVS strategies that aid in the mechanization of abstraction proofs. These strategies first set up the standard subgoals for the abstraction proofs and then execute the standard initial proof steps for these subgoals, thus making the process of proving abstraction properties in PVS more automated. With suitable supplementary strategies to implement the “natural” proof steps needed to complete the proofs of any of the standard subgoals remaining to be proved, the abstraction proof strategies can form part of a set of mechanized proof steps that can be used interactively to translate high level proof sketches into PVS proofs. Using timed I/O automata examples taken from the literature, this paper illustrates use of the templates, theories, and strategies described to specify and prove two types of abstraction property: refinement and forward simulation.     

Abstractions of Hamiltonian control systems

Given a control system and a desired property, an abstracted system is a reduced system that preserves the property of interest while ignoring modeling detail. In previous work, abstractions of linear and nonlinear control systems were considered while preserving reachability properties. In this paper, we consider the abstraction problem for Hamiltonian control systems, where, in addition to the property of interest we also preserve the Hamiltonian structure of the control system. We show how the Hamiltonian structure of control systems can be exploited to simplify the abstraction process. We then focus on local accessibility preserving abstractions, and provide conditions under which local accessibility properties of the abstracted Hamiltonian system are equivalent to the local accessibility properties of the original Hamiltonian control system.     

On the Specification of Higher Dimensional Automata

Higher dimensional automata (HDA) have been widely studied as models of concurrent processes. Most current work focuses on developing the directed algebraic topological notions required to analyse HDA to determine their computer scientific properties (deadlock, safety, unreachable states, etc). Instead, this paper is concerned with the software engineering of HDA and details the specification of HDA by process algebra operations. The specifications work for cubical HDA, but are designed to also work for the explicit choice higher dimensional automata (ECHDA) originally proposed by Buckland. We introduce ω-multigraphs, a graphical notion which is easier to use than pasting schemes but more general than cubical complexes, we describe basic process algebra operations on ECHDA as constructions on ω-multigraphs, we discuss the trichotomy of concurrent, conferring, and conflicting choices, and note that the “deadlock choice” can arise from intersecting conflicting choices, and we remark that common software engineering refinements correspond to choice refinement.     

A paris-model approach to modular simulation

The development of complex models can be greatly facilitated by the utilization of libraries of reusable model components. In this paper we describe an object-oriented module specification formalism (MSF) for implementing archivable modules in support of continuous spatial modeling. This declarative formalism provides the high level of abstraction necessary for maximum generality, provides enough detail to allow a dynamic simulation to be generated automatically, and avoids the “hard-coded” implementation of space-time dynamics that makes procedural specifications of limited usefulness for specifying archivable modules. A set of these MSF modules can be hierarchically linked to create a parsimonious model specification, or “parsi-model”. The parsi-model exists within the context of a modeling environment (an integrated set of software tools which provide the computer services necessary for simulation development and execution), which can offer simulation services that are not possible in a loosely-coupled “federated” environment, such as graphical module development and configuration, automatic differentiation of model equations, run-time visualization of the data and dynamics of any variable in the simulation, transparent distributed computing within each module, and fully configurable space-time representations. We believe this approach has great potential for bringing the power of modular model development into the collaborative simulation arena.     

A model checking-based approach for security policy verification of mobile systems

This article describes an approach for the automated verification of mobile systems. Mobile systems are characterized by the explicit notion of location (e.g., sites where they run) and the ability to execute at different locations, yielding a number of security issues. To this aim, we formalize mobile systems as Labeled Kripke Structures, encapsulating the notion of location net that describes the hierarchical nesting of the threads constituting the system. Then, we formalize a generic security-policy specification language that includes rules for expressing and manipulating the code location. In contrast to many other approaches, our technique supports both access control and information flow specification. We developed a prototype framework for model checking of mobile systems. It works directly on the program code (in contrast to most traditional process-algebraic approaches that can model only limited details of mobile systems) and uses abstraction-refinement techniques, based also on location abstractions, to manage the program state space. We experimented with a number of mobile code benchmarks by verifying various security policies. The experimental results demonstrate the validity of the proposed mobile system modeling and policy specification formalisms and highlight the advantages of the model checking-based approach, which combines the validation of security properties with other checks, such as the validation of buffer overflows.