Performance modelling of a network processor using POOSL

The increasing complexity of innovative real-time hardware/software systems forced industry to consider system-level design methods. Before actually implementing a system with hardware and software components, system-level design methods enable analysing the performance of different design alternatives that realise the required functionality. In order to develop performance models early in the design process, the parallel object-oriented specification language (POOSL) can be used. POOSL is an expressive modelling language for analysing complex real-time distributed hardware/software systems. Being equipped with a formal semantics, POOSL ensures unambiguous execution of models and proper application of performance analysis techniques. This paper discusses the use of POOSL for analysing the performance of a network processor. A network processor consists of components that perform their behaviour in a synchronously concurrent way, whereas POOSL is based on an asynchronous modelling paradigm. In this paper, we illustrate that constructing abstract models of synchronous systems for the purpose of performance analysis may benefit from an asynchronous modelling approach.     

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.     

Formal Verification of Dynamic Properties in an Aerospace Application

Formal verification of computer-based engineering systems is only meaningful if the mathematical models used are derived systematically, recording the assumptions made at each modelling stage. In this paper we give an exposition of research efforts in cooperation with aerospace industries in Sweden. We emphasize the need for modelling techniques and languages covering the whole spectrum from informal engineering documents, to hybrid mathematical models. In this modelling process we give as much weight to the physical environment as to the controlling software. In particular, we report on our experience using switched bond graphs for the modelling of hardware components in hybrid systems. We present the basic ideas underlying bond graphs and illustrate the approach by modelling an aircraft landing gear system. This system consists of actuating hydromechanic and electromechanic hardware, as well as controlling components implemented in software and electronics. We present a detailed analysis of the closed loop system with respect to safety and timeliness properties. The proofs are carried out within the proof system of Extended Duration Calculus.     

An approach to formal verification of human–computer interaction

The correct functioning of interactive computer systems depends on both the faultless operation of the device and correct human actions. In this paper, we focus on system malfunctions due to human actions. We present abstract principles that generate cognitively plausible human behaviour. These principles are then formalised in a higher-order logic as a generic, and so retargetable, cognitive architecture, based on results from cognitive psychology. We instantiate the generic cognitive architecture to obtain specific user models. These are then used in a series of case studies on the formal verification of simple interactive systems. By doing this, we demonstrate that our verification methodology can detect a variety of realistic, potentially erroneous actions, which emerge from the combination of a poorly designed device and cognitively plausible human behaviour.     

HYPE: Hybrid modelling by composition of flows

Hybrid systems are manifest in both the natural and the engineered world, and their complex nature, mixing discrete control and continuous evolution, make it difficult to predict their behaviour. In recent years several process algebras for modelling hybrid systems have appeared in the literature, aimed at addressing this problem. These all assume that continuous variables in the system are modelled monolithically, often with differential equations embedded explicitly in the syntax of the process algebra expression. In HYPE an alternative approach is taken which offers finer-grained modelling with each flow or influence affecting a variable modelled separately. The overall behaviour then emerges as the composition of flows. In this paper we give a detailed account of the HYPE process algebra, its semantics, and its use for verification of systems. We establish both syntactic conditions (well-definedness) and operational restrictions (well-behavedness) to ensure reasonable behaviour in HYPE models. Furthermore we consider how the equivalence relation defined for HYPE relates to other relations previously proposed in the literature, demonstrating that our fine-grained approach leads to a more discriminating notion of equivalence. We present the HYPE model of a standard hybrid system example, both establishing that our approach can reproduce the previously obtained results and demonstrating how our compositional approach supports variations of the problem in a straightforward and flexible way.     

Analysing neurobiological models using communicating automata

Two important issues in computational modelling in cognitive neuroscience are: first, how to formally describe neuronal networks (i.e. biologically plausible models of the central nervous system), and second, how to analyse complex models, in particular, their dynamics and capacity to learn. We make progress towards these goals by presenting a communicating automata perspective on neuronal networks. Specifically, we describe neuronal networks and their biological mechanisms using Data-rich Communicating Automata, which extend classic automata theory with rich data types and communication. We use two case studies to illustrate our approach. In the first case study, we model a number of learning frameworks, which vary in respect of their biological detail, for instance the Backpropagation (BP) and the Generalized Recirculation (GeneRec) learning algorithms. We then used the SPIN model checker to investigate a number of behavioral properties of the neural learning algorithms. SPIN is a well-known model checker for reactive distributed systems, which has been successfully applied to many non-trivial problems. The verification results show that the biologically plausible GeneRec learning is less stable than BP learning. In the second case study, we presented a large scale (cognitive-level) neuronal network, which models an attentional spotlight mechanism in the visual system. A set of properties of this model was verified using Uppaal, a popular real-time model checker. The results show that the asynchronous processing supported by concurrency theory is not only a more biologically plausible way to model neural systems, but also provides a better performance in cognitive modelling of the brain than conventional artificial neural networks that use synchronous updates. Finally, we compared our approach with several other related theories that apply formal methods to cognitive modelling. In addition, the practical implications of the approach are discussed in the context of neuronal network based controllers.     

Formal verification of a pervasive messaging system

As ubiquitous computing becomes a reality, its applications are increasingly being used in business-critical, mission-critical and even in safety-critical, areas. Such systems must demonstrate an assured level of correctness. One approach to the exhaustive analysis of the behaviour of systems is formal verification, whereby each important requirement is logically assessed against all possible system behaviours. While formal verification is often used in safety analysis, it has rarely been used in the analysis of deployed pervasive applications. Without such formality it is difficult to establish that the system will exhibit the correct behaviours in response to its inputs and environment. In this paper, we show how model-checking techniques can be applied to analyse the probabilistic behaviour of pervasive systems. As a case study we apply this technique to an existing pervasive message-forwarding system, Scatterbox. Scatterbox incorporates many typical characteristics of pervasive systems, such as dependence on sensor reliability and dependence on context. We assess the dynamic temporal behaviour of the system, including the analysis of probabilistic elements, allowing us to verify formal requirements even in the presence of uncertainty in sensors. We also draw some tentative conclusions concerning the use of formal verification for pervasive computing in general.     

Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B

We demonstrate refinement-based formal development of the hybrid, ‘fixed virtual block’ approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. Our approach uses iUML-B diagrams as a front end to the Event-B modelling language. We use abstraction to verify the principle of movement authority before gradually developing the details of the Virtual Block Detector component in subsequent refinements, thus verifying that it preserves the safety properties. We animate the refined models to demonstrate their validity using the scenarios from the Hybrid ERTMS Level 3 (HLIII) specification. We reflect on our team-based approach to finding useful modelling abstractions and demonstrate a systematic modelling method based on the state and class diagrams of iUML-B. The component and control flow architectures of the application, its environment and interacting systems emerge through the layered refinement process. The runtime semantics of the specification’s state-machine behaviour are modelled in the final refinements. We discuss how the model could be used to generate an implementation using code generation tools and techniques.

     

Verification Approach of Metropolis Design Framework for Embedded Systems

In this paper, we focus on the verification approach of Metropolis, an integrated design framework for heterogeneous embedded systems. The verification approach is based on the formal properties specified in Linear Temporal Logic (LTL) or Logic of Constraints (LOC). Designs may be refined due to synthesis or be abstracted for verification. An automatic abstraction propagation algorithm is used to simplify the design for specific properties. A user-defined starting point may also be used with automatic propagation. Two main verification techniques are implemented in Metropolis the formal verification utilizing the model checker Spin and the simulation trace checking with automatic generated checkers. Translation algorithms from specification models to verification models, as well as algorithms of generated checkers are discussed. We use several case studies to demonstrate our approach for verification of system level designs at multiple levels of abstraction.     

Behavioural equivalence in simulation modelling

Discrete event simulation has grown up as a practical technique for estimating the quantitative behaviour of systems, where direct measurement is undesirable or impractical. It is also used to understand the detailed functional behaviour of such systems. Its theory is largely that of experimental science, centering on statistical approaches to validation, rather than on the verification of detailed behaviour. On the other hand, much work has been done on understanding and proving functional properties of systems, using techniques of formal specification and concurrency modelling. This article presents an approach to understanding equivalence of behaviour of discrete event simulation models, using a technique from the concurrency world, Milner’s Calculus of Communicating Systems (CCS). This yields a significant advance over the main previous work, Schruben and Yücesan’s simulation graphs. CCS allows for the use of observational equivalence, which can capture a more flexible, behavioural notion of equivalence than the structural equivalence defined there.A common framework based on the process view of models is constructed, using a hierarchical graphical modelling language (Extended Activity Diagrams). This language is shown to map onto both the major constructs of the DEMOS discrete event simulation language and the corresponding CCS models. A graphically driven tool based on such a framework is presented, which generates both types of models. Using the CCS model, behavioural equivalences and differences in simulation models are demonstrated.     

On the interpretation of local models in blended multiple model structures

The construction of non-linear dynamics by means of interpolating the behaviour of locally valid models offers an attractive and intuitively pleasing method of modelling non-linear systems. The approach is used in fuzzy logic modelling, operating regime based models, and non-linear statistical models. The model structure suggests that the composite local models can be used to interpret, in some appropriate manner, the overall non-linear dynamics. In this paper we demonstrate that the interpretation of these local models, in the context of multiple model structures, is not as straightforward as it might initially appear. We argue that the blended multiple model system can be interpreted in two ways as an interpolation of linearizations, or as a full parameterization of the system. The choice of interpretation affects experiment design, parameter identification, and model validation. We then show that, in some cases, the local models give insight into full model behaviour only in a very small region of state space. More alarmingly, we demonstrate that for off-equilibrium behaviour, subject to some approximation error, a non-unique parameterization of the model dynamics exists. Hence, qualitative conclusions drawn from the behaviour of an identified local model, e.g. regarding stable, unstable, nodal or complex behaviour, must be treated with extreme caution. The example of muscle modelling is used to illustrate these points clearly.     

Gaussian process approach for modelling of nonlinear systems

Parametric modelling principals such as neural networks, fuzzy models and multiple model techniques have been proposed for modelling of nonlinear systems. Research effort has focused on issues such as the selection of the structure, constructive learning techniques, computational issues, the curse of dimensionality, off-equilibrium behaviour, etc. To reduce these problems, the use of non-parametrical modelling approaches have been proposed. This paper introduces the Gaussian process (GP) prior approach for the modelling of nonlinear dynamic systems. The relationship between the GP model and the radial basis function neural network is explained. Issues such as selection of the dimension of the input space and the computation load are also discussed. The GP modelling technique is demonstrated on an example of the nonlinear hydraulic positioning system.     

Verification of reactive systems using temporal logic with clocks

This paper presents a framework for the specification and verification of timing properties of reactive systems using Temporal Logic with Clocks (TLC). Reactive systems usually contain a number of parallel processes, therefore, it is essential to study and analyse each process based on its own local time. TLC is a temporal logic extended with multiple clocks, and it is in particular suitable for the specification of reactive systems. In our framework, the behavior of a reactive system is described through a formal specification; its timing properties, including safety and liveness properties, are expressed by TLC formulas. We also propose several demonstration techniques, such as an application of local reasoning and deriving fixed-time rules from the proof system of TLC, for proving that a reactive system meets its temporal specification. Under the proposed framework, the timing properties of a reactive system can therefore be directly reasoned about from the formal specification of the system.     

Verification and analysis of domain-specific models of physical characteristics in embedded control software

ContextA considerable portion of the software systems today are adopted in the embedded control domain. Embedded control software deals with controlling a physical system, and as such models of physical characteristics become part of the embedded control software.ObjectiveDue to the evolution of system properties and increasing complexity, faults can be left undetected in these models of physical characteristics. Therefore, their accuracy must be verified at runtime. Traditional runtime verification techniques that are based on states/events in software execution are inadequate in this case. The behavior suggested by models of physical characteristics cannot be mapped to behavioral properties of software. Moreover, implementation in a general-purpose programming language makes these models hard to locate and verify. Therefore, this paper proposes a novel approach to perform runtime verification of models of physical characteristics in embedded control software.MethodThe development of an approach for runtime verification of models of physical characteristics and the application of the approach to two industrial case studies from the printing systems domain.ResultsThis paper presents a novel approach to specify models of physical characteristics using a domain-specific language, to define monitors that detect inconsistencies by exploiting redundancy in these models, and to realize these monitors using an aspect-oriented approach. We complement runtime verification with static analysis to verify the composition of domain-specific models with the control software written in a general-purpose language.ConclusionsThe presented approach enables runtime verification of implemented models of physical characteristics to detect inconsistencies in these models, as well as broken hardware components and wear and tear of hardware in the physical system. The application of declarative aspect-oriented techniques to realize runtime verification monitors increases modularity and provides the ability to statically verify this realization. The complementary static and runtime verification techniques increase the reliability of embedded control software.     

Compositional analysis for verification of parameterized systems

Many safety-critical systems that have been considered by the verification community are parameterized by the number of concurrent components in the system, and hence describe an infinite family of systems. Traditional model checking techniques can only be used to verify specific instances of this family. In this paper, we present a technique based on compositional model checking and program analysis for automatic verification of infinite families of systems. The technique views a parameterized system as an expression in a process algebra (CCS) and interprets this expression over a domain of formulas (modal mu-calculus), considering a process as a property transformer. The transformers are constructed using partial model checking techniques. At its core, our technique solves the verification problem by finding the limit of a chain of formulas. We present a widening operation to find such a limit for properties expressible in a subset of modal mu-calculus. We describe the verification of a number of parameterized systems using our technique to demonstrate its utility.     

Modelling socio-ecological systems with MAIA: A biogas infrastructure simulation

Similar to other renewable energy technologies, the development of a biogas infrastructure in the Netherlands is going through social, institutional and ecological evolution. To study this complex evolutionary process, we built a comprehensive agent-based model of this infrastructure. We used an agent-based modelling framework called MAIA to build this model with the initial motivation that it facilitates modelling complex institutional structures. The modelling experience however proved that MAIA can also act as an integrated solution to address other major modelling challenges identified in the literature for modelling evolving socio-ecological systems. Building on comprehensive reviews, we reflect on our modelling experience and address four key challenges of modelling evolving socio-ecological systems using agents: (1) design and parameterization of models of agent behaviour and decision-making, (2) system representation in the social and spatial dimension, (3) integration of socio-demographic, ecological, and biophysical models, (4) verification, validation and sensitivity analysis of such ABMs.     

Verification and control of partially observable probabilistic systems

We present automated techniques for the verification and control of partially observable, probabilistic systems for both discrete and dense models of time. For the discrete-time case, we formally model these systems using partially observable Markov decision processes; for dense time, we propose an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. We give probabilistic temporal logics that can express a range of quantitative properties of these models, relating to the probability of an event’s occurrence or the expected value of a reward measure. We then propose techniques to either verify that such a property holds or synthesise a controller for the model which makes it true. Our approach is based on a grid-based abstraction of the uncountable belief space induced by partial observability and, for dense-time models, an integer discretisation of real-time behaviour. The former is necessarily approximate since the underlying problem is undecidable, however we show how both lower and upper bounds on numerical results can be generated. We illustrate the effectiveness of the approach by implementing it in the PRISM model checker and applying it to several case studies from the domains of task and network scheduling, computer security and planning.     

Bayesian statistical model checking with application to Stateflow/Simulink verification

We address the problem of model checking stochastic systems, i.e., checking whether a stochastic system satisfies a certain temporal property with a probability greater (or smaller) than a fixed threshold. In particular, we present a Statistical Model Checking (SMC) approach based on Bayesian statistics. We show that our approach is feasible for a certain class of hybrid systems with stochastic transitions, a generalization of Simulink/Stateflow models. Standard approaches to stochastic discrete systems require numerical solutions for large optimization problems and quickly become infeasible with larger state spaces. Generalizations of these techniques to hybrid systems with stochastic effects are even more challenging. The SMC approach was pioneered by Younes and Simmons in the discrete and non-Bayesian case. It solves the verification problem by combining randomized sampling of system traces (which is very efficient for Simulink/Stateflow) with hypothesis testing (i.e., testing against a probability threshold) or estimation (i.e., computing with high probability a value close to the true probability). We believe SMC is essential for scaling up to large Stateflow/Simulink models. While the answer to the verification problem is not guaranteed to be correct, we prove that Bayesian SMC can make the probability of giving a wrong answer arbitrarily small. The advantage is that answers can usually be obtained much faster than with standard, exhaustive model checking techniques. We apply our Bayesian SMC approach to a representative example of stochastic discrete-time hybrid system models in Stateflow/Simulink: a fuel control system featuring hybrid behavior and fault tolerance. We show that our technique enables faster verification than state-of-the-art statistical techniques. We emphasize that Bayesian SMC is by no means restricted to Stateflow/Simulink models. It is in principle applicable to a variety of stochastic models from other domains, e.g., systems biology.