Simulink is popular tool used widely in industry to model and simulate dynamic systems, for example, embedded systems. A Simulink model is a connected bl ock diagram that represent a set of mathematical functions specifying systems. The graphical environment of Simulink assists users to quickly design systems. Simulink provides powerful numerical integration mechanism to visually validate system performanc e by simulation. A simulation represents the system behavior under a particular circumstance, namely, specific parameter values, explicit input functions, fixed simulation period.

However, with the increasing usage of embedded systems in safety-critical, real-time environment, higher-level assurance and timing analysis become more important. Simulink is deficient to check requirements over infinite situations, for example, a parameter value over an uncountable range. It is also hard to specify and reason timing requirements in Simulink. Moreover, open systems are not analyzable since the input functions must be known exactly in Simulink for the sake of simulation.

Hence, we look at the possible help from formal specification languages, which can model systems at an abstract level with rigorous semantics, and analyze system behavior against complex requirements formally. Timed Interval Calculus (TIC) is chosen. The formal notation is based on set theory, and reuses well-known Z mathematical and schema notations. It has been applied to model and reason many real-time systems. The inspiration of our approach comes from that both Simulink and TIC describe system behavior in terms of continuous-time semantics.

Our goal is to apply TIC to complement Simulink. In this work, we firstly translate Simulink models into TIC specifications. The translation preserves the functional and timing aspects. Next, we specify important timing requirements using the tra nslated TIC specifications. The requirements can be over exactly the whole system or just some of its components, and hence this way can increase the design space. Last but not least, we can check that system design satisfies requirements by making use of the well-defined TIC reasoning rules. Consequently, we can elevate the design confidence in Simulink.

• Associate Professor and Assistant Dean: Jin Song Dong
• PhD Candidate: Chunqing Chen

A Simulink model is constructed in a hierarchical order. Namely, the leaves are elementary blocks. They denote the primitive mathematical functions, such as integration, addition and so on. The elementary blocks are produced by Simulink library blocks. Each library block can generate different elementary blocks in a specific model with the use of parameterization technique. Namely, different parameter values determine different functionalities of the elementary blocks. Blocks in Simulink are connected by arrowed wires. A wire denotes the dependence relationship between the connected blocks. A model is thus is a connected block diagram, and it can also contain other submodels that are blocks whi ch consists of blocks with wires, too.

We select Timed Interval Calculus (TIC) to complement Simulink. The formal notation is set-theory based, and reuses Z mathematical and schema no tations. In TIC specifications, variables are total functions over time. Terms formed by variables and constants are interpreted as functions from time to real numbers. In turn predicates constructed by terms with propositional logic operators, and a pred icate is indeed a boolean-valued function over time. In TIC, an interval is a set of continuous time instances. TIC defines special brackets to return a set of specific intervals, in each of which, the enclosed predicate holds everywhere. A TIC formula is thus an expression which constrains the relationships among different sets of intervals with the use of conventional set operators. To manage TIC specifications, we adopt Z schema structure to group TIC formulas over a list of variables with their declar ed types. Hence, TIC specifies system behavior in terms of intervals.

To accomplish our goal, there are three steps as shown below:

1. Define a set of TIC library functions for a set of Simulink library blocks: The TIC library functions modeling the behavior of Simulink library blocks. They serve the similar role as library blocks, that is to say, they are the templates to create TIC specifications to represent elementary blocks during the translation.

2. Develop a strategy to translate Simulink models into TIC specifications: The translation is in the bottom-up order. Each elementary block is converted into a schema, which retains the functional and timing aspects. Each wire is denoted by an equat ion. A model is translated into a schema, that captures the structure of the diagram.

3. Analyze generated TIC specifications against requirements described in TIC: Requirements are formed based on the translated TIC specifications. Hence we can link the requirements with systems directly. Furthermore, complex timing requirements are supported beyond Simulink. Making use of the TIC reasoning rules, we can formally check whether a system design logically implies requirements.

In the following, we explain the solutions in details. In the end, one pure continuous system and one hybrid system are provided as experiments.

Simulink provides a rich set of library blocks to generate elementary blocks as the units of the models. Unfortunately, they are informally described in the documentation, which illustrate their behavior under simulation. To avoid the ambiguity, we concern the denotational semantics of the blocks. Namely, the input-output mathematical relation denoted by the library block. Moreover, Simulink interprets system behavior in terms of continuous time, so the timing feature, to be specific, the sample time, the rate at which the block executes during the simulation, should be retained in the TIC specification s.

In general, a TIC library function models a functionality of a library block.

• Arguments relate to the Simulink operand parameters and sample time. They are assigned specific numerical value in models, and they hence won't affect the functionality of the produced elementary blocks.

• A schema is returned. The schema aims to depict the behavior of the corresponding elementary block. Inputs, output and relevant parameters are defined in the declaration part. The predicate part constrains the timing relationships over the declare d variables.

  • If the elementary block is assigned the continuous sample time, i.e., the block executes at all time points. We lift the constraint from time point level into a higher level, i.e. intervals.

  • If the elementary block is assigned the sample time, the block updates its function at sampling time points, and keep constant within the period between two adjacent sampling time points. We decompose the time domain int o a sequence of left-closed, right-open intervals. The length of each interval equals the sample time value. The discrete update behavior is represented by restricting that the output within the interval depends on only the input value at the beginning.

Currently, there are 54 TIC library functions to handle 33 often-used Simulink library blocks from 8 categories, such as continuous, discrete, and discontinuous libraries. A report on how to define TIC library functions in general and the explicit specifications can be found here.

As Simulink models are constructed hierarchically, the translation is in the bottom-up order. Namely, the analysis starts from the elementary blocks, and then wires, followed by (sub)models.

1. Each elementary block is translated into a schema. The schema is generated by applying relevant Simulink parameters to a TIC library function. Two factors are taken into accoun t:

   • The selection criteria decides which TIC library function is appropriate to model the library block. The basic criterion is the Simulink parameter BlockType that indicates the type of the library block. The criteria also includes the relat ed operator parameters since they can affect the functionality.
   • The timing feature is the sample time of each elementary block. In a specific model, the sample time of an elementary block can be:

     • assigned explicitly by the block parameter SampleTime or
     • implied by the type of the library block. E.g., instances of continuous or library blocks have the sample time value 0.
     • derived by the sample time propagation
2. Each wire is translated into an equation of two schema variables. The variables denote the interface of the connected blocks. In this way, the equivalence of two functions over time remains the non-blocked communication feature in Simulink. Na mely, the value read by the destination block is the one written by the source block at the same time.
3. A (sub)model is translated into a schema. The schema is based on other schemas generated for its components. Hence, the structure of the model is preserved in the schema. To be specific, the components are declared as instances of the pre-tran slated schemas, and the connections are constrained by a set of equations.

After the translation, we can specify important requirements exactly on the systems or their components. The requirement specifications are formed in terms of the translated TIC specif ications. Hence, this way directly links the requirements and Simulink models. Thanks to the expressive power of TIC, complex timing requirements beyond Simulink can be modelled easily.

We aim to make use of the formal validation capability of TIC to elevate the design confidence of Simulink. In TIC, a validation is a deduction to show that the design logically implies the requirement. Usually a proof starts from the hypothesis, and moves in a forward processing manner. During the proof, each deductive step can be reached by applying one of the following:

• A TIC formula from the translated TIC specification. Since the generated TIC specifications preserves the functional and timing aspects of the original Simulink models, a TIC formula thus represents either a functional behavior of the block o r a connection in the model.
• A mathematical law. As a predicate in TIC is in first order logic, common mathematical logics can be used freely. Moreover, TIC supports the modelling of integral and differential calculus, so conventional control theory can be applied to cop e with continuous dynamics.
• A pre-proved theorem of elementary blocks or submodels. Simulink model is formed in a hierarchical order, so we often decompose complex requirements into sub-requirements over submodels. Thus, the proved sub-requirements serve as lemmas durin g the higher level analysis.
• A TIC reasoning rule. There are 18 well-defined rules capturing the properties of intervals and sets of intervals. With the usage of these rules, we can handle complex proofs.

We remark that open systems are checkable provided certain constraints of their input functions are known. These systems are not analyzable in Simlink because the input functions of systems must be known exactly for the sake of simu lation. In our approach, the constraints are treated as assumptions during the validation.

We use the following two non-trivial models to show our approach in details.

• Heater model
• Water tank model

Last updated 10/08/2006.