Contract-based verification of MATLAB-style matrix programs

MATLAB/Simulink is a popular toolset for developing embedded software. The main target of the toolset is numerical computing applications and the tools offer a rich language for manipulating matrices. This paper presents an approach to automatic, modular, contract-based verification of programs written in a subset of the MATLAB programming language. We focus on efficient handling of the built-in matrix manipulation functions commonly used in MATLAB. We restrict ourselves to the subset of MATLAB suitable for code generation, which means matrix types and shapes can be determined statically. We present an approach to static type and shape inference for matrices that is more strict than MATLAB, but aids verification. The type and shape information is then used in the verification. From the programs and contracts we generate verification conditions that are discharged with an off-the-shelf SMT solver. We discuss two approaches to encode matrix functions and evaluate them on a number of examples. We also investigate the use of k-induction to decrease the need for user annotations. We found our approach to be efficient for programs that manipulate relatively small matrices, which are common in embedded applications.     

Contract-based modeling and verification of timed safety requirements within SysML

In order to cope with the growing complexity of critical real-time embedded systems, systems engineering has adopted a component-based design technique driven by requirements. Yet, such an approach raises several issues since it does not explicitly prescribe how system requirements can be decomposed on components nor how components contribute to the satisfaction of requirements. The envisioned solution is to design, with respect to each requirement and for each involved component, an abstract specification, tractable at each design step, that models how the component is concerned by the satisfaction of the requirement and that can be further refined toward a correct implementation. In this paper, we consider such specifications in the form of contracts. A contract for a component consists in a pair (assumption, guarantee) where the assumption models an abstract behavior of the component’s environment and the guarantee models an abstract behavior of the component given that the environment behaves according to the assumption. Therefore, contracts are a valuable asset for the correct design of systems, but also for mapping and tracing requirements to components, for tracing the evolution of requirements during design and, most importantly, for compositional verification of requirements. The aim of this paper is to introduce contract-based reasoning for the design of critical real-time systems made of reactive components modeled with UML and/or SysML. We propose an extension of UML and SysML languages with a syntax and semantics for contracts and the refinement relations that they must satisfy. The semantics of components and contracts is formalized by a variant of timed input/output automata on top of which we build a formal contract-based theory. We prove that the contract-based theory is sound and can be applied for a relatively large class of SysML system models. Finally, we show on a case study extracted from the automated transfer vehicle (http://www.esa.int/ATV) that our contract-based theory allows to verify requirement satisfaction for previously intractable models.     

Transformation of Simulink models to IEC 61499 Function Blocks for verification of distributed control systems

In this paper, a new model-based engineering approach is introduced by bridging MATLAB Simulink with IEC61499 Function Block models. This is achieved by a transformation between the two block-diagram languages. The transformation supported by the developed tools sets the cornerstone of the verification and validation framework for IEC 61499 Function Blocks in closed-loop with the models of the plant. The framework also paves the way to running distributed simulations of complex hybrid (i.e., continuous-discrete) closed-loop plant-controller systems and building complex models using the efficient object instantiation techniques of IEC 61499.     

p-Automata: New foundations for discrete-time probabilistic verification

We introduce p-Automata, which are automata that accept languages of Markov chains, by adapting notions and techniques from alternating tree automata to the realm of Markov chains. The set of languages of p-automata is closed under Boolean operations, and for every PCTL formula it contains the language of the set of models of the formula. Furthermore, the language of every p-automaton is closed under probabilistic bisimulation. Similar to tree automata, whose acceptance is defined via two-player games, we define acceptance of Markov chains by p-automata through two-player stochastic games. We show that acceptance is solvable in EXPTIME; but for automata that arise from PCTL formulas acceptance matches that of PCTL model checking, namely, linear in the formula and polynomial in the Markov chain. We also derive a notion of simulation between p-automata that approximates language containment in EXPTIME and is complete for Markov chains. These foundations therefore enable abstraction-based probabilistic model checking for probabilistic specifications that subsume Markov chains, and LTL and CTL* like logics.     

Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories

Automatic verification of programs and computer systems with input variables represents a significant and well-motivated challenge. The case of Simulink diagrams is especially difficult, because there the inputs are read iteratively, and the number of input variables is in theory unbounded. We apply the techniques of explicit model checking to account for the temporal (control) aspects of verification and use set-based representation of data, thus handling both sources of non-determinism present in the verification. Two different representations of sets are evaluated in scalability with respect to the range of input variables. Explicit (enumerating) sets are very fast for small ranges but fail to scale. Symbolic sets, represented as first-order formulas in the bit-vector theory and compared using satisfiability modulo theory solvers, scale well to arbitrary (though still bounded) range of input variables. To leverage the combined strengths of explicit and symbolic representations, we have designed a hybrid representation which we showed to outperform both pure representations. Thus, the proposed method allows complete automatic verification without the need to limit the non-determinism of input. Moreover, the principle underlying the hybrid representation entails inferring knowledge about the system under verification, which the developers did not explicitly include in the system, and which can significantly accelerate the verification process.     

State-space forms for higher-order discrete-time models

This paper presents a fundamental study of the connection between continuous- and discrete-time systems. Provided is a definition for discrete-time models, that is discrete-time systems with a continuous-time counterpart, whose order can be higher than that of the continuous-time system. This definition is based on a comparison in a certain sense on the time responses of continuous- and discrete-time systems. A theorem is presented for relating the higher-order discrete-time models to their continuous-time counterparts, which is an extension of a previous theorem for models with order equal to that of the continuous-time system. State-space forms are derived for models obtained through the use of a certain class of hold elements and through the use of mapping models, and these discrete-time systems are shown to be valid according to the definition. Special cases are models obtained using first-order and slewer hold devices, whose convergence to a continuous-time counterpart has not been shown mathematically before, and mapping models corresponding to two-step linear multi-step methods, which have not previously presented in the state-space form. The derived state-space forms provide a convenient way to implement these models for purposes of analysis, design, and implementation of discrete-time systems and finds applications in such areas as digital signal processing, digital simulation, and digital control.     

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.     

Adaptive control of discrete-time systems using multiple models

The adaptive control of a linear time-invariant discrete-time system using multiple models is considered in this paper. Both the deterministic (noise free) case and the stochastic case when random disturbances are present are discussed. Based on the prediction errors of a finite number of fixed and adaptive identification models, a procedure is outlined for switching between a finite number of controllers to improve performance. The principal contributions of the paper are the proof of global stability of the overall system and the convergence of the tracking error signal to zero in the deterministic case and the proof of convergence of the minimum variance control problem. Computer simulation results are included to complement the theoretical results     

Delta sum state estimation for discrete-time dynamical models

Optimal recursive estimates are derived for a class of non-Gaussian nonlinear systems using a discrete approximation of the probability density function of the measurement noise.     

Parameter estimation for linear discrete-time models with randomcoefficients

The problem of parameter estimation in linear discrete-time systems with random coefficients is discussed. In particular, the maximum-likelihood estimators and their consistency for the defined structure of the model are derived. The estimators have a structure similar to that of the least square estimators for the linear discrete-time system with constant coefficients     

Exploring models for semantic category verification

Many artificial intelligence tasks, such as automated question answering, reasoning, or heterogeneous database integration, involve verification of a semantic category (e.g. “coffee” is a drink, “red” is a color, while “steak” is not a drink and “big” is not a color). In this research, we explore completely automated on-the-fly verification of a membership in any arbitrary category which has not been expected a priori. Our approach does not rely on any manually codified knowledge (such as WordNet or Wikipedia) but instead capitalizes on the diversity of topics and word usage on the World Wide Web, thus can be considered “knowledge-light” and complementary to the “knowledge-intensive” approaches. We have created a quantitative verification model and established (1) what specific variables are important and (2) what ranges and upper limits of accuracy are attainable. While our semantic verification algorithm is entirely self-contained (not involving any previously reported components that are beyond the scope of this paper), we have tested it empirically within our fact seeking engine on the well known TREC conference test questions. Due to our implementation of semantic verification, the answer accuracy has improved by up to 16% depending on the specific models and metrics used.     

Modeling slotted WDM rings with discrete-time Markovian models

An approximate discrete-time Markov chain model is developed for an all-optical WDM ring in which users transmit fixed-length packets (or cells) according to the SRR (Synchronous Round Robin) medium access control protocol. The model steady-state solution allows the computation of the traditional performance parameters of interest, i.e., through-puts and average delays, for packets referring to specific source–destination pairs. The comparison of the model results with the outputs of a detailed simulator shows that the two different approaches provide very similar forecasts about the network performance parameters. This indicates that traditional modeling approaches can offer important contributions in the design of modern high-speed networks.     

Optimal expansions of discrete-time Volterra models using Laguerre functions

This work is concerned with the optimization of Laguerre bases for the orthonormal series expansion of discrete-time Volterra models. The aim is to minimize the number of Laguerre functions associated with a given series truncation error, thus reducing the complexity of the resulting finite-dimensional representation. Fu and Dumont (IEEE Trans. Automatic Control 38(6) (1993) 934) indirectly approached this problem in the context of linear systems by minimizing an upper bound for the error resulting from the truncated Laguerre expansion of impulse response models, which are equivalent to first-order Volterra models. A generalization of the work mentioned above focusing on Volterra models of any order is presented in this paper. The main result is the derivation of analytic strict global solutions for the optimal expansion of the Volterra kernels either using an independent Laguerre basis for each kernel or using a common basis for all the kernels.     

A new perspective for discrete-time models of a continuous-timesystem

Various discrete-time models of a continuous-time system are given an interpretation in terms of the system structures and the hold device. This concept provides a novel perspective of various discrete-time models and a simple way to understand the relationships which exist among those models, but which are not easily visualized without the proposed interpretation. This interpretation of discrete-time models also allows the creation of new types of models. Tables of discrete-time models, including the newly developed ones, are provided     

Fractional discrete-time consensus models for single- and double-summator dynamics

The leader–following consensus problem of fractional-order multi-agent discrete-time systems is considered. In the systems, interactions between opinions are defined like in Krause and Cucker–Smale models but the memory is included by taking the fractional-order discrete-time operator on the left-hand side of the nonlinear systems. In this paper, we investigate fractional-order models of opinions for the single- and double-summator dynamics of discrete-time by analytical methods as well as by computer simulations. The necessary and sufficient conditions for the leader–following consensus are formulated by proposing a consensus control law for tracking the virtual leader.     

On the generalized q-Markov cover models for discrete-time systems

A new method for obtaining generalized q-Markov cover models for discrete-time SISO systems is proposed and is based on the inverse solution of the Lyapunov equation. The reduced order models not only match the Markov parameters and high-frequency power moments like the conventional q-Markov cover techniques but also match time moments and low-frequency power moments of the original system     

Construction of discrete-time models for port-controlled Hamiltonian systems with applications

The issues of constructing a discrete-time model for Hamiltonian systems are in general different from those for dissipative systems. We propose an algorithm for constructing an approximate discrete-time model, which guarantees Hamiltonian conservation. We show that the algorithm also preserves, in a weaker sense, the losslessness property of a class of port-controlled Hamiltonian systems. An application of the algorithm to port-controlled Hamiltonian systems with quadratic Hamiltonian is presented, and we use this to solve the stabilization problem for this class of systems based on the approximate discrete-time model constructed using the proposed algorithm. We illustrate the usefulness of the algorithm in designing a discrete-time controller to stabilize the angular velocity of the dynamics of a rigid body.     

Identification of discrete-time state affine state space models using cumulants

This paper is concerned with the identification of discrete-time, time invariant, state affine state space models driven by an independent identically distributed (IID) random input, and in the presence of process and measurement noise. The identification problem is treated using a cumulant based approach. It is shown that the input-output and input-state crosscumulant equations in the time domain have the form of a linear autonomous system. An algorithmic procedure is then developed, for the computation of the unknown system matrices, based on a standard deterministic linear subspace identification algorithm, provided the input signal has some persistent excitation properties. The special case of Gaussian IID input is also examined. The proposed method is computationally very efficient and its accuracy is illustrated by simulations.     

Statistical evaluation and verification of digital simulation models

In most instances, designers of digital simulation models ignore the statistical design and the statistical implications associated with these models. Most ignore the problem because of the added difficulties related to autocorrelated data. Fishman and Kiviat of the RAND Corporation [33] suggested the use of spectral analysis as a technique for evaluating the significance of statistics emanating from a simulation model, comparing model output with “real-world” data for model verification and comparing model outputs for two or more policy change evaluations. The authors have developed this concept into a synthesized model and verified the model through a spectral analysis on data derived from the Logistics Composite Model (LCOM). LCOM was developed jointly by the RAND Corporation and the Air Force Logistics Command for the purpose of simulating aircraft flight and base support processes in response to mission requirements. Some forty statistics were evaluated through spectral analysis for confidence limits. Further, certain policy changes regarding inventory re-order were implemented and a spectral analysis was performed to judge whether or not the separate results were statistically different.     

Lightweight and static verification of UML executable models

Executable models play a key role in many software development methods by facilitating the (semi)automatic implementation/execution of the software system under development. This is possible because executable models promote a complete and fine-grained specification of the system behaviour. In this context, where models are the basis of the whole development process, the quality of the models has a high impact on the final quality of software systems derived from them. Therefore, the existence of methods to verify the correctness of executable models is crucial. Otherwise, the quality of the executable models (and in turn the quality of the final system generated from them) will be compromised. In this paper a lightweight and static verification method to assess the correctness of executable models is proposed. This method allows us to check whether the operations defined as part of the behavioural model are able to be executed without breaking the integrity of the structural model and returns a meaningful feedback that helps repairing the detected inconsistencies.