Tabular requirements assist with the specification of software requirements using an “if-then” paradigm and are supported by many tools. For example, the Requirements Table block in Simulink®supports writing executable specifications that can be used as test oracles to validate an implementation. But even before the development of an implementation, automatic checking of consistency and completeness of a Requirements Table can reveal errors in the specification. Fixing such errors earlier than in later development cycles avoids costly rework and additional testing efforts that would be required otherwise. As of version R2022a, Simulink®supports checking completeness and consistency of Requirements Tables when the requirements are stateless, that is, do not constrain behaviors over time. We overcome this limitation by considering Requirements Tables with both stateless and stateful requirements. This paper (i) formally defines the syntax and semantics of Requirements Tables, and their completeness and consistency, (ii) proposes eight encodings from two categories (namely, bounded and unbounded) that support stateful requirements, and (iii) implementsTheano, a solution supporting checking completeness and consistency using these encodings. We empirically assess the effectiveness and efficiency of our encodings in checking completeness and consistency by considering a benchmark of$160$Requirements Tables for a timeout of two hours. Our results show thatTheanocan check the completeness of all the Requirements Tables in our benchmark, it can detect the inconsistency of the Requirements Tables, but it can not confirm their consistency within the timeout. We also assessed the usefulness ofTheanoin checking the consistency and completeness of 14 versions of a Requirements Table for a practical example from the automotive domain. Across these 14 versions,Theanocould effectively detect two inconsistent and five incomplete Requirements Tables reporting a problem (inconsistency or incompleteness) for$50\%$(7 out of 14) versions of the Requirements Table.

Simulation-based software testing supports engineers in finding faults in Simulink®models. It typically relies on search algorithms that iteratively generate test inputs used to exercise models in simulation to detect design errors. While simulation-based software testing techniques are effective in many practical scenarios, they are typically not fully integrated within the Simulink environment and require additional manual effort. Many techniques require engineers to specify requirements using logical languages that are neither intuitive nor fully supported by Simulink, thereby limiting their adoption in industry. This work presentsHECATE, a testing approach for Simulink models using Test Sequence and Test Assessment blocks from Simulink®Test™. Unlike existing testing techniques,HECATEuses information from Simulink models to guide the search-based exploration. Specifically,HECATErelies on information provided by the Test Sequence and Test Assessment blocks to guide the search procedure. Across a benchmark of$18$Simulink models from different domains and industries, our comparison ofHECATEwith the state-of-the-art testing toolS-Taliroindicates thatHECATEis both more effective (more failure-revealing test cases) and efficient (less iterations and computational time) thanS-Talirofor$\approx$94% and$\approx$83% of benchmark models respectively. Furthermore,HECATEsuccessfully generated a failure-revealing test case for a representative case study from the automotive domain demonstrating its practical usefulness.

Simulink and Stateflow are tools for Model-Based Design that support a variety of mechanisms for modeling hybrid dynamics. Each of these tools has different strengths. In this paper, a new modeling construct is presented that combines these strengths to enable graphical modeling of hybrid dynamics within a single Stateflow chart. A new type of Stateflow state that acts as a Simulink subsystem is developed to facilitate graphical modeling of continuous dynamics using Simulink blocks inside Stateflow. Remote textual and graphical state access using new state-accessor blocks enables continuous states to be used in transition guards and reset actions. Key features of this new formalism are illustrated using various examples with hybrid dynamics.

No abstract available.

In model-based development, abstraction provides insight and tractability. Different formalisms are often used at different levels of abstraction to represent the variety of concerns that need to be addressed when designing complex cyber-physical systems. In this paper, we consider the problem of establishing abstraction across heterogeneous formalisms in a compositional manner. We use the framework of behavioral semantics to elucidate the general conditions that must be satisfied to assure that the composition of abstractions for individual components is an abstraction for the composition of the components. The theoretical concepts are illustrated using an example of a cooperative intersection collision avoidance system (CICAS).

Today's complex cyber-physical systems are being built increasingly using model-based development (MBD), where mathematical models for the system behavior are checked against design specifications using analysis tools. Different types of models and analysis tools are used to address different aspects of the system. While the use of heterogeneous formalisms supports a divide-and-conquer approach to complexity and allows engineers with different types of expertise to work on various aspects of the design, system integration problems can arise due to the lack of an underlying unifying formalism. In this paper, we introduce the notion of behavior relations to address the problem of heterogeneity and propose constraints over parameters as a mechanism to manage inter-model dependencies and ensure consistency. In addition, we present structured constructs of nested conjunctive and disjunctive analyses to enable multi-model heterogeneous verification. The theoretical concepts are illustrated using an example of a cooperative intersection collision avoidance system (CICAS).

We present an approach for verifying locking of charge-pump phase-locked loops by performing reachability analysis on a behavioral model of the circuit. Bounded uncertain parameters in the behavioral model make it possible to represent all possible behaviors of more detailed models. The dynamics of the behavioral model is hybrid (i.e., discrete and continuous) due to the switching of charge pumps that drive the analog control circuits. A unique feature of phase-locked loops compared to most other hybrid systems is that they require thousands of switchings in the continuous dynamics to converge sufficiently close to a limit cycle. This makes reachability analysis a challenging task since switches in the dynamics are expensive to compute and result in conservative overapproximations. We solve this problem by overapproximating the effects of the switching conditions with uncertain parameters in linear continuous models, a method we call continuization. Using efficient reachability algorithms for discrete-time linear systems, locking is verified over the complete range of possible initial states of a charge-pump PLL designed in 32nm CMOS SOI technology in comparable time required for Monte Carlo simulations of the same behavioral model.