VerSÅA user manual⋆
Contents
1. used for other purposes The function transpose has to be used instead Note also that that the equals operator is and assignment operator is VerSAA complains about unknown blocks VerSAA can only handle a subset of the Simulink blocks See Table 1 for a list of supported blocks See also the previous section on how to deal with the situation Note that even the built in Simulink blocks are sometimes library blocks included in models as references VerSAA cannot handle library blocks so the best option is to inline all reference blocks before attempting verification VerSAA complains about unknown identifiers Check that all variables are spelled correctly in the contract Also check that all references to block mem ories in the invariant section are done correctly VerSAA only obtains variable values from the Matlab workspace when run from Matlab Therefore all block parameters which are not numeric values used in a diagram need to be declared in the contract of a containing subsystem otherwise VerSAA complains that it cannot derive sampling rates The inference of sampling times in VerSAA is more strict than in Simulink It also essentially only works forward in the model This means that typically all constant blocks and inports on the highest level in the subsystem hierarchy need to have sampling times given Rate transition blocks also have to be used to connect parts of the model with different sampling times VerSAA complain2. invariant Second part bool2real delay delay delay Bool 0 0 0 B2 X amp amp bool2real delay delay delay delay Bool 0 0 0 0 B3 X end A delay expression has the same sampling as the port that it delays Using delay expressions is recommended over explicitly declared memories since it usually results in specifications that are shorter and easier to read Note also 6 See 2 1 for this way to specify memory of subsystems e098 VerSAA BinToDecDelayDescriptionNotCorrect mdl B BinToDecDelayDescriptionNotCorrect mdl Result v 7 Bool I rt sg i Ada Curd Verification results for BO UnitDelay subsystem BinSeqToDec B1 UnitDelay B2 UnitDelay B3 UnitDelay BinSeqToDec initisalisation Constant Constant Constantl Constant Factor Constant _ Factorl Constant Factor2 Constant _ Factor3 Constant Product Product Productl Product Product2 Product Product3 Product Rate Transition RateTransition Switch Switch Output should be within limits E BinSeqToDec Decimal_0_ lt 4 Correct BinSeqToDec Incorrect Failed assertions Decimal Outport Output should be within limits BinSeqToDec Decimal_O_ gt 2 Fig 5 Result of verifying the BinToDec model where some postconditions do not hold that initialisation the zeros can be omitted as long as the delay is initialised at least
3. a variable or port v can be declared to be a 3x2 ma trix using the notation v matrix double 3 2 The notation v matrix double 3 states that v is a 3x1 matrix column vector The first index gives the number of rows and the second the number of columns To do the dimension inference the dimensions must be numeric constants Hence writing v matrix double N N is not allowed unless the parameter N is defined in the Matlab Workspace the value of N is then used in the inference and VerSAA is used from Matlab This also means that matrix creation functions such as zeros ones etc need to have arguments that are numeric constants or the parameters can be directly found in the Matlab workspace One significant difference from Simulink is that VerSAA does not do implicit type conversions In particular the indices in matrices and vectors are integers int32 This means that all expressions used as matrix indices must be of type integer and not double Explicit type conversion blocks or functions must be used otherwise Matrices are translated to two dimensional arrays in Z3 There are two ways to verify programs that use matrices The default approach is to use axioms defining the properties of the supported functions This works well in some cases However if functions that have recursive definitions are used then performance will be poor This is fairly common e g matrix multiplication functions sum prod min etc with one arg
4. file lt tool folder gt config functions def The user can add functions definitions here Note also the pattern declaration pat for each condition in the file This is used by Z3 as hints for how to instantiate the quantifiers 4 8 Common issues VerSAA complains about syntax errors The following problems are com mon The arguments for the range operator have to be constants which is checked already at the syntactic level Also syntax such as a 2 for indexing Function Table 2 List of the supported functions Assumption Arithmetic opertaors can only be applied to scalars gt gt amp amp a b c a c min max abs sgn square sqrt sin cos tan pow saturate to_real to_int intXX uintXX isinteger bool2real real2bool size length zeros ones all any sum prod min max transpose factorial sum_up Relational operators Only and can be applied to booleans Logical operators The arguments have to be booleans The range operator works as in Matlab but the arguments a b and c must be numeric constants The range indexing operator works as in Matlab but it can only be used to index a whole row or column Here c must be a scalar Va t y t min a y if x lt y then z else y end Vz t y t max x y if x gt y then z else y end Vz t abs x if 0 lt x then z else x end Va t sgn x if 0 z then 0 else if
5. min and maz Trigonometry See below for which functions are supported Relational Operator All alternatives are supported but only and works for booleans Signum Abs Unary Minus Switch Comparing with 0 also works for booleans Constant If a type of the output is given in the block it is respected Unit Delay Memory Dead Zone Saturate Bias Datatype conversion Support conversion between most types Multiport Switch Supports arbitrary many inputs Index Vector Matrix Selector Mux and Demux Width Rate transition This is the only block that tolerates different rates on the ports Backlash Enabled subsystems The enable port block is then also supported Merge For iterator subsystems The limitations discussed earlier applies InPort amp OutPort stored in an XML file lt tool folder gt config functions xml The format of the XML file is described in 2 This file contains the list of all blocks that are currently supported as well as the behaviour they are assumed to have However it is currently not possible to just add new block definitions to this file The reason is that the blocks also need to be known by the typechecker This is something that will be fixed in the future There is an option for handling blocks that have no definitions in VerSAA The verification of a subsystem relies on contract descriptions of subsystems lower in the subsystem hierarchy If an unknown block is encapsulated in a subsystem with a contra
6. often arithmetic intensive Conceptually the calculations are usually then carried out using real arithmetic However in Simulink these calculations are then often implemented using floating point arithmetic according to IEEE 754 standard Verification involving floating point computation is hard 7 For example Simulink Design Verifier approximates floating point arithmetic with rational number arithmetic 6 We also approx imate floating point numbers with real numbers This approach helps to show that the principles of the system are correct However many defects relating to when the behaviour of floating point and real arithmetic differ will go unde tected This problem is not just theoretical as rounding errors commonly cause significant problems with accuracy of the results of calculations 6 Examples To get a better idea of how VerSAA can be used to verify different types of properties about Simulink models a few small examples are given 6 1 A multi rate Simulink model The following multi rate model computes decimal value of the four latest binary inputs delayed by one The output is updated on a rate four times slower than the input Hence the sampling period of the input is one while the sampling period of the output is four time units The diagram implementing the functionality is shown in Figure 4 The contract is written in the Description field of the Block properties of the subsystem In order to remember the four last i
7. once In the invariant we need to say how block memories relate to the delays We refer to the memory of e g the delay block BO as BO X To refer to a block B in a subsystem S the syntax S B is used The result from verifying the model with VerSAA can be seen in Figure 5 The command used was here slverifier gui lt BinToDec model gt The entire model is verified when running VerSAA on a model The user interface is divided into two parts a tree view to the left and a text box to the right The tree view shows an overview of the verification results of the Simulink model while the text box can show more detailed information for the chosen subsystem The subsystems with contracts are marked in different colors in the tree view depending on the verification result Green The subsystem is correct C 1 gt eraio For Iterator r r_old Fig 6 A Simulink diagram from a for iterator subsystem to compute the sum of all natural numbers up to n Red The subsystem is incorrect The properties that were not verified are shown to the right By writing properties separately with good descriptions it is easier to locate the problem precisely to some simple condition Orange The status of the subsystem is unknown Also here the properties that were not verified are shown to the right Gray The subsystem could not be verified This is typically because the subsystem contained some block
8. sufficiently large library of supported blocks to make the tool useful for verification of real systems The limitations are currently VerSAA supports verification of multi rate subsystems where each rate has zero phase Furthermore only the rate transition blocks can have inputs and outputs of different rates This is similar to Simulink Design Verifier VerSAA only supports a subset of the Simulink blocks The list of blocks supported by VerSAA can be found in Section 7 VerSAA supports only a subset of the built in Matlab functions The list of built in Matlab functions supported by VerSAA can be found in Section 7 5 2 Matrix and vector support VerSAA has support for calculations using matrices and vectors see 9 for details The goal is that the operators and functions should handle multi dimensional data in the same manner as Matlab Simulink Note that matrices and vectors are not allowed to be dynamically resized but this is not recom mended in embedded code anyway The syntax is also simplified in order to al low more efficient automated verification and many of the more unusual ways to index elements in matrices are not supported Dimensions of signals are inferred as in normal Simulink Note that only up to 2 dimensional signals are supported Furthermore VerSAA has only matrices vectors are 1xN or Nx1 matrices and the special array type in Simulink is not used An NxM matrix has N rows and M columns For example
9. they have to be given the cor rect type not the default double if that is not the desired type of course Check that all ports in the contracts have correct names corresponds to the ones in the subsystems Non matching names can give strange type errors VerSAA complains about matrix dimensions even though the Simulink approves of them Also here VerSAA is more strict There is no array type in VerSAA and all vectors are either n x 1 or 1 x n vectors so this has to be handled carefully VerSAA returns the result Unknown even though the subsystem seems to be correct Z3 is only a semi decision procedure in many cases Thus some times it cannot verify that some property holds even though it does One useful trick is to assign concrete values to parameters to eliminate non linear arithmetic or reduce the amount of it In case the tool is called from Matlab then param eter definitions from the Matlab root workspace will be used which should help One can also give concrete values to the inports in the precondition in order to verify the system for some specific input values Note that for incorrect models where matrices or non linear arithmetic is used unknown will often be reported Z3 will often also get stuck in an infinite loop then References 1 P Bostr m Contract based verification of Simulink models In ICFEM2011 volume 6991 of LNCS Springer 2011 2 P Bostr m R Gr nblom T Huotari and J Wiik An approach to
10. unrolls loops when checking iteration and fixed loop bounds need to be provided This is more restrictive than VerSAA but it is still useful for embedded software where the number of iterations should have a strict upper bound Also no loop invariants need to be provided when unrolling loops Note that VerSAA does not currently prove termination of loops it proves partial correctness 7 Supported blocks and functions Supported blocks A relatively large number of blocks are supported The supported structuring mechanisms are Atomic subsystems virtual normal sub systems enabled subsystems and for iterator subsystems A list of the supported builtin blocks is given in Table 1 Additionally almost all sink blocks are also supported However their behaviour is not modelled The block definitions are T Embedded Matlab in Simulink models is actually a Stateflow chart with a Embedded Matlab function embedded hence it is not supported in verification of Simulink models Table 1 List of the supported blocks Block Comment Sum Supports arbitrary number of inputs as well as giving operators for ports Product Supports arbitrary many ports as well as giving operators for ports see limitations for x and in Table 2 Gain Supports both elementwise and matrix multiplication Logic Supports AND OR and NOT Arbitrary many inputs for AND and OR supported Math See Table 2 for supported functions MinMax Supports both one and two input version of
11. SAA includes the SMT solver Z3 This means the tool cannot be used commercially unless the user already has a commer cial license for Z3 See VerSAA xx z3 LICENSE txt for details 4 Running the tool Enter the folder lt tool folder gt VerSAA Windows Run slverifier bat lt params gt lt simulink model file gt Unix Linux and Mac OS X Run slverifier sh lt params gt lt simulink model file gt Work done in The DiHy project coordinated by Fimecc and funded by Tekes 1 VerSAA can be run independently of Matlab Simulink or from within Matlab In Matlab The tool can also be used from Matlab by calling the function slverifier m This function takes two argument the first is the model name and the second is a cell array of strings giving the parameters The command help slverifier gives detailed information As described above the program is a command line program that takes a Simulink model as argument There are a number of parameters that can be given to the program An overview all the different parameters are given here in order to have a complete list in one place In the examples shown later more in depth presentation of what the tool actual does will be given log all off This parameter enable control of how much information the tool will print out When log all is used a lot of debugging information will be printed For users most will be of little interest gui Shows the result of the verification
12. The verification conditions are such that they are only valid hold for all vari able values if the subsystem is correct The SMT solver Z3 is used to auto matically show validity Z3 3 4 has background theories for many constructs needed in embedded systems such as linear and non linear arithmetic linear integer arithmetic arrays bitvectors etc The properties that can be proved is largely dependent on this tool Z3 is only a semi decision procedure for some theories and thus it cannot always decide if a formula is valid or not The result of the verification in VerSAA can be Correct the verified subsystem is correct Incorrect the verified subsystem is incorrect Then the failed conditions are displayed As a failed condition can be identified fairly precisely it should give a good indication of where the problem is located Unknown Z3 cannot decide if the subsystem is correct or incorrect This often occurs if a subsystem is incorrect but an undecidable theory like non linear real arithmetic is used 5 Capabilities VerSAA can do verification of multi rate Simulink models and a relatively small subset of Embedded Matlab It can handle multi dimensional data which is typically used in control and signal processing applications This section gives an overview of the capabilities and limitations of the tool 5 1 General limitations The subset of Simulink supported by VerSAA is not complete However there is a
13. VerSAA user manual Pontus Bostrom Department of Information Technologies Abo Akademi University Joukahaisenkatu 3 5 20520 Turku Finland pontus bostrom abo fi 1 Introduction This document gives an overview on how to use VerSAA which is a tool for au tomatically verifying correctness of Simulink models with respect contract anno tations The document starts with installation instruction Then an overview of the contract format and the capabilities of VerSAA are given This is followed by a few examples on how to verify different aspects of a number of small systems The last two sections give a reference of supported blocks and functions as well as advice on handling common issues 2 Installing and running the program VerSAA is a program written in Java that consists of collection of jar files and some additional scripts to conveniently run the tool The tool is run from the command line but it can display results from the verification graphically Installation instructions 1 Ensure that that a JVM at least Java 1 6 is installed One can be down loaded from http java com Note that for a 64 bit version of VerSAA a 64 bit version of Java is needed 2 Unpack the downloaded VerSAA package in a desired folder This will create a folder VerSAA xx where xx is the version with all the files No further installation steps are needed The folder containing the program can also be moved freely 3 Note that this version of Ver
14. contract based verification of Simulink models Technical Report 985 Turku Centre for Computer Science TUCS 2010 3 L de Moura and N Bj rner Z3 an efficient SMT solver In Tools and Algorithms for the Construction and Analysis of Systems TACAS2008 volume 4963 of LNCS pages 337 340 Budapest Hungary 2008 Springer 4 L de Moura and N Bj rner Z3 a tutorial http research microsoft com en us um redmond projects z3 5 F Maraninchi and L Morel Logical time contracts for reactive embedded compo nents In 30th EUROMICRO Conference on Component Based Software Engineer ing Track ECBSE 04 Rennes France August 2004 6 Mathworks Inc Simulink http www mathworks com products simulink 2010 7 D Monniaux The pitfalls of verifying floating point computations ACM Transac tions on Programming Languages and Systems TOPLAS 30 3 2008 8 J Wiik Contract based verification of multi rate Simulink models Master s thesis Abo Akademi University 2012 9 J Wiik and P Bostr m Contract based verification of MATLAB and Simulink matrix manipulating code Technical Report 1107 TUCS 2014
15. ct describing its behaviour VerSAA can use the contract information to verify the rest of the model However as the content of that subsystem the unknown block cannot be analysed VerSAA cannot check that the subsystem correctly satisfies its contract The correctness has to be verified e g by testing or with Simulink Design Verifier As the correctness has to be verified externally the contract must be written carefully to not introduce false assumptions More generally VerSAA will not verify subsystems with contracts that contain unknown blocks However it will use the contract descriptions when verifying the rest of the model This enables verification of large models where some parts might contain unsupported constructs Supported functions A number of functions from Matlab are also supported There are two classes of supported functions The first class is completely sup ported functions where VerSAA knows the function definition The second class is functions where VerSAA will treat the function as an uninterpreted function symbol However VerSAA might contain assumptions about the function The currently supported functions as well as the assumptions known about them are listed in Table 2 The table gives the function definitions for elementwise functions when real scalar numbers are used The definitions are straightforward to extend to matrices All supported functions with corresponding assumptions known about them is given in the
16. d The contracts for for iterator subsystems are a bit different than for normal subsystems The idea here is that the for iterator subsystem computes a function where the inports are arguments and the outports provides the results there is no state remembered between invocations here The contract cannot contain delay expressions or specification variables memories 1 The memories of the blocks in the diagram are used to store intermediate results To verify the for loop we need a loop invariant that describes the intermediate results The loop invariant captures the situation between loop iterations We construct the loop invariant in such a manner that when the invariant holds and the loop has finished the loop guard does not hold anymore then that implies the desired postcondition The idea in the verification is that if we assume that the loop invariant holds before an arbitrary iteration and then check that it holds after then it will always hold between iterations Then in the final step we prove that given that the invariant holds when the loop has terminated the desired post condition has been reached Note that a loop index variable k is automatically defined and can be used in the invariant Here we prove inductively that the block memory r_old X contains the intermediate result during the execution of the loop Note also that the invariant in this case can refer to the inports The postcondition then only relates inputs and output
17. e its input output behaviour since the output depends on the internal state given by the Unit Delay blocks We use a delay of the first light light1 to say that the light is unchanged if timeout is false and flipped if timeout is true The initialisation of this light is here assumed to be red false The postconditions then encode the desired behaviour of the controller The invariant in invariant then describes how the memories in the Unit delay blocks in the subsystems LS1 and L92 relate to the delay delay light1 The invariant also states that the lights always have different color Here a function v is used to map block memories to variable identifiers This mapping is discussed more in the examples in Section 6 The concrete syntax used in the contract conditions is inspired by the syntax of Matlab expressions 2 4 Principles for verification The approach to verification is described in detail in 1 8 2 Here only a brief overview is given Simulink is used to develop control systems where the in teraction of programs with their environment rather than their input output behaviour is important Hence we are here interested in reactive systems where the execution of the behaviour of the Simulink model is observed during exe cution We can observe the value of a port or block memory only at the time points when it is sampled Note that Simulink is only guaranteed to behave in this manner for discrete models with fixed step solver In o
18. e g Stateflow the tool did not understand By clicking on a desired subsystem in the tree view more information is provided to the right In Figure 5 the subsystem Bin2Dec has two failed assertion The postcondition Output should be within limits does not hold The real lower limit is 0 and the real upper limit is 15 The failed assertions are shown to the right Note that since VerSAA handles multi rate models the buffer index for the port the problem occurred is also given In this case it is the first sample directly which is denoted by the suffix _0_ after the port name 6 2 A for iteration subsystem This example involves a for iterator subsystem that computes the sum of all natural numbers up to a limit given as parameters We have first defined the function sum_up This function is defined recursively We have the following axioms Va int32 x gt 0 sum_up x sum_up a 1 1 sum_up 0 0 2 The verification of the subsystem will also proves the well known formula sum_up n n n 1 2 Contents of the subsystem is shown in Figure 6 The inport n gives the number to sum up to and the outport gives the result The delay block stores the intermediate values The contract for this subsystem is given as contract inports n int32 outports r int32 requires n gt 0 ensures r sum_up n amp amp r n n 1 to_int32 2 invariant r_old X sum_up k 1 amp amp r_old X k k 1 to_int32 2 en
19. ed for real verification tasks as well An example of an Embedded Matlab program is given in Fig 8 and more examples can be found in 9 The function of interest is max_f that finds the maximum element in the array a Note that in order to infer numeric dimensions the program need to have dimensions on all parameters given Hence the small function test_maz that calls the function max_f is needed Here max_f is tested for a 10 x 1 vector One can think of it as exhaustive testing of the function for a vector of a specific size Specifications are given after since then the specifications will be com ments in Matlab and the functions are valid Matlab code The first specification regards type parameters as the functions are polymorphic The function works for any numeric type t double int32 int16 and for any dimension n The parameter a is then declared to be of type matrix t n 1 meaning a matrix with element of type t and dimension n x 1 The return value is then a scalar a 1 x 1 matrix of type t There is no precondition The postcondition states that all elements of a are smaller or equal to m and that there exists an element in a equal to m The implementation is essentially a while loop where the minimum element is searched for Note that we initialise the loop index i to be of type int32 This is necessary since integers need to be used as indices into matrices Here it is easy to find the loop invariant We say in the inva
20. ed to search for violations over only a finite time In VerSAA an inductive invariant has to be given explicitly for the internal state given in the invariants clause of the contract Given this invariant and inputs satisfying the precon ditions then the postcondition and the invariant is established Furthermore VerSAA supports refinement based compositional verification for building cor rectness arguments for large systems function x test_max a types x double a matrix double 10 1 x max_f a end function m max f a typeparameters t lt numtype n int32 types m t a matrix t n 1 ensures all a lt m 9 ensures any a m 10 m a 1 11 i int32 2 12 while i lt length a 13 invariant 1 lt i amp amp i lt n 1 14 invariant forall j int32 1 lt j amp amp j lt i gt m gt a j 15 invariant exists j int32 1 lt j amp amp j lt i amp amp m a j oo NOONA WNEHE 16 if m lt a i 17 m a i 18 end 19 i i 1 20 end 21 end Fig 8 A MATLAB function for finding the index of the minimum element in a column vector annotated with contracts VerSAA via Z3 supports non linear arithmetic better than SLDV However currently VerSAA does not support common Simulink features such as Stateflow and embedded MATLAB which SLDV supports The support for matrix data seems fairly weak in SLDV where scalability is often poor 9 Furthermore SLDV
21. elves contain diagrams Here we use contracts 2 to give a high level functional description of these subsystems Simulink can model continuous discrete and hybrid systems The verification methods described here concern discrete periodic systems which is one of the most common forms of control software Note that multi rate models are supported However they have to have the phase also called offset part of the sampling time set to zero To illustrate the use of Simulink a small example that consists of a controller for a simplified traffic light system is given The system consists of two lights that can be either green true or red false However both lights should not be green at the same time When a timeout signal has the value true the lights change The subsystem block TLC in Fig 1 a contains the traffic light controller A new light configuration is computed separately for each light by the subsystems LS1 and LS2 Fig 1 b at each sampling instant Both lights are switched in case timeout is true otherwise they retain their values Fig 1 c 3 1 Verification based on contracts Contracts describe valid behaviours of atomic subsystems in Simulink models i e what are valid outputs in response to valid inputs VerSAA verifies that a given Simulink subsystem annotated by a contract also satisfies it To add a contract to a subsystem the contract is written down in the Description field4 of that subsystem The abstract sy
22. in a graphical user interface This parameter is recommended when the tool is used to verify Simulink models nowf Do not do well formedness checks When this parameter is used the tool will not check absence of divisions by zero square root of negative numbers etc underflows or overflows for integer arithmetic operation as well as index out of bounds matrix accesses psdf Print the sdf graphs that are generated in the verification generation process They are produced as pdf files in the working directory Note that the tool Dot which is part of the Graphviz package is used for generating the pictures WARNING Any file with matching name will be overwritten This is mostly useful for debugging of the verification process and it is not useful for users expand This enables expansion of all matrix operators This is the recom mended method for verifying models and programs that use matrix calcula tions on small matrices When VerSAA is used from Matlab it will use variables in the Matlab workspace That is if a variable in the workspace is used in the Simulink model the value it has in the workspace is used in the verification VerSAA can also be used to verify Embedded Matlab code In that case the argument to the verifier is an m file Note that only a relatively small subset of Embedded Matlab is supported The support is aimed at providing a more simple environment than Simulink to experiment with verification of Mat
23. n optional descrip tion Here Q describes the block parameters used in the subsystem Q is the precondition describing the valid inputs and Q is the postcondition describing valid outputs In the contract conditions it is also possible to refer to old input and output values The syntax delay x i denotes the previous sample of port x with the initial value i To verify the subsystem it is then necessary to describe how these old port values are actually represented in the Simulink implementation The condition Q is used to describe how the delayed ports relate to block memories in the subsystem diagram This condition describes a property that is invariant during system execution This invariant property is the only thing remembered between sampling instances so it has to carry enough information to enable the correctness proof The contracts here have a similar structure and can describe the same type of behaviour as the ones for reactive components in 5 To give an idea of how contracts can be used a contract describing the functionality of the traffic light system from Fig 1 is given in Fig 2 b We want to prove that both lights are not green at the same time that is light1 light2 We also want to say that the lights are only changed when the input timeout is true The contract first declares the inputs and outputs together with their type To give an accurate description of the system we cannot just describ
24. nputs delay expressions are used Delay expressions can only be used to delay inports or outports or delays of them This restriction is to simplify handling of sampling times The contract is shown below contract inports Bool boolean outports Decimal double ensures Main condition 5 This is handled in Simulink by returning mathematically incorrect but useful re sults s gt x Factor3 gt Product 3 1 B3 z A 4 gt io Factor2 Product 2 1 m e B2 x p gt A A neds p Decimal gt agg Rate Transition Factorl gt Product1 1 B1 z 1 gt 3 Factor Product 1 Bo z 1 0 Constant Bool aa Qa seek gt Switch 0 0 Constant1l Fig 4 A Simulink diagram implementation of the binary to decimal converter Decimal bool2real delay Bool 0 1 bool2real delay delay Bool 0 0 2 bool2real delay delay delay Bool 0 0 0 4 bool2real delay delay delay delay Bool 0 0 0 0 8 ensures Output should be within limits Decimal lt 4 Decimal gt 2 invariant First part bool2real delay Bool 0 BO X amp amp bool2real delay delay Bool 0 0 B1 X
25. ntax of contracts is shown in Fig 2 a There c u and y are identifiers and t is a type in the set double int32 int16 int8 uint32 uint16 uint8 boolean or matrices containing these types E g a ma trix of type double and dimensions nx m is declared as matrix double n m Then t Right click on the subsystem choose block properties contract parameters c1 t1 3Cn itn inports u1 t1 Un tn outports y t Yn tn paramcondition Description Q requires Description Q x ensures Description Q invariant Description Q end param y inv contract inports timeout boolean outports light1 boolean light2 boolean ensures Properties of the first light timeout gt light1 delay light1 false timeout gt light delay light1 false ensures One light is always red light1 light2 invariant delay light1 v LS1 ls amp amp v LS2 ls v LS1 ls end a b Fig 2 a The abstract syntax of contracts and b an example contract that describes the traffic light controller subsystem zx denotes zero or more occurrences of z and Q denotes a predicate The con tract first declares the parameters in and out ports of the subsystem These are all given as lists of identifier type pairs The behaviour of the subsystem is described by a set of conditions Each condition can have a
26. of the contract conditions are formed by combinations of states and port values It is easy to check that they hold for each transition model execution As already mentioned VerSAA checks that each time the model is executed it behaves according to the contract specification of the subsystems The correct ness is verified one subsystem at the time This will guarantee that the complete model will be correct 1 The verification is thus compositional For each dia gram D in subsystem with a contract the tool checks that when the internal diagram is executed in a state where the invariant on the internal state holds then for any input satisfying the precondition the diagram will establish the postcondition and invariant again For multi rate models we cannot only look at one execution of a subsystems but we have to check the property at least for the shortest repeating behaviour This means for a time period of the least common multiple of the sampling periods as offsets phases on sampling times are not allowed For multi rate model the invariant should then hold for all time instants when the subsystem behaviour repeats i e for the period that is the least common multiple of the periods of the inputs and outputs The technical details of the verification can be found in 2 8 1 9 The principle in VerSAA is that the verification should be completely auto matic For each subsystem a number of verification conditions are generated
27. oof is needed which might be stronger than the property of interest This means that this approach might require more manual work than approach 1 Fig 3 A state machine used for demonstrating the principle behind verification Consider the simple Simulink subsystem modelling a traffic light controller in Figure 1 The internal state of that model is given by the unit delay blocks LS1 ls and LS2 ls We model the state as the tuple LS1 ls LS2 ls The states in the model now correspond to the states in the transition system as follows sl true false s2 true true s3 false true s4 false false The ports labels p are given by the tuple of inport and outport values timeout light1 light2 Here we have that p11 false true false pl4 true false true p44 false false true p41 true true false p22 false true true p23 true false false This shows how one can view the Simulink model as a labelled transition system As can be seen from the transition system rep resentation a state where both lights are switched on at the same time can not be reached from the initial state When using approach 2 for verification a suitable property invariant is P s s1 V s s3 or in other words P LS1 ls LS2 ls as also stated in the contract in Fig 2 b From any such state we can then show that for any input on timeout the model will end up in such a state again after execution The rest
28. riant that m is the minimum element in vector a up to index 7 We also need to state the bounds on 7 When the loop guard does not hold anymore then i n 1 and then according to the loop invariants m is the minimum of the whole vector a Finding the loop invariants can be very challenging for more complicated programs However in more complex algorithms the same information is usually captured in diagrams describing the situations between loops Then it is just a matter of expressing this information formally Note that VerSAA does not check that the loops actually terminate Hence VerSAA checks partial correctness which means that it only guarantees that if all the functions terminate the result produced is correct Termination checks could be added to VerSAA but at the moment they are not supported In the case of the for iterator subsystem termination is guaranteed by behaviour of the subsystem under the restrictions used in VerSAA 6 5 Comparision with Simulink Design Verifier From a user point of view the biggest difference between the tools is proba bly that verification conditions and assumptions are given as special blocks in Simulink Design Verifier SLDV The verification approach is quite similar in VerSAA and Simulink Design Verifier SLDV uses an approach based on k induction where it tries to infer some invariant over a number of steps and then verify that the model satisfies the invariant Bounded model checking can also us
29. rix code Verification of code that use matrices and vectors is discussed in Section 5 2 3 Simulink and contracts The language used to create models in Simulink is based on hierarchical data flow diagrams 6 see e g Fig 1 A Simulink diagram consists of functional blocks 2 In order for the built in JVM in Matlab to find Z3 it is necessary to set java library path to include the folder VerSAA z3 bin See the Matlab documen tation on how to do this 3 Graphviz http www graphviz org S light timeout light C1 2 gt timeout timeout light1 Ig i LS1 light2 C 5 a 4 NOT TLE timeout light C2 timeout Switch1 Is Logical a light2 Operator Ls2 b c Fig 1 a A subsystem that contains a simple traffic light controller b its contents consisting of two individual light controllers and c the individual light controllers connected by signals wires The blocks represent transformations of data while the signals give the flow of data between blocks Blocks can be parameterised with parameters that are set before model execution and remain constant during the execution Blocks can also contain memory Hence their behaviour do not only depend on the current values on the inputs and the parameter values but also on previous input values The diagrams can be hierarchically structured using the notion of subsystem blocks which are blocks that thems
30. s Based on the invariant we can then prove the postcondition when we know we just exited the loop We have the following restrictions for for iterator subsystems Only one based indexing is supported The iteration limit has to be given as an inport The increment is one and not given as a inport Memories are reset at the start of every execution of the block 6 3 Finding the minimum element in a vector This example illustrates the use of multi dimensional data The example consists of a for iterator subsystem that returns the minimum value v and the index i of the minimum value from a vector a The diagram for the subsystem is shown in Fig 7 The contract is given as contract inports a matrix double 1 N outports i int32 v double ensures Index limits 0 gt Nest Width For Iterator x lt PH 0 Index Relational i Vector Operator Switch a 1 Lo la E ector ind LAO v Index Vector 2 Fig 7 A Simulink diagram for a for iterator subsystem to find the minimum element of a vector a 1 lt i amp amp i lt length a ensures Properties of min index all a i lt a ensures Properties of min value a i v invariant 1 lt k amp amp k lt length a 1 lt ind X amp amp ind X lt length a forall j int32 1 lt j amp amp j l
31. s about type errors even though the Simulink ap proves of the typing The type inference algorithm in VerSAA might not produce exactly the same typing as the one in Simulink The typing in VerSAA is more strict in order to generate efficient verification conditions for the verifier There are a number of things to consider Doubles and integers cannot be mixed in computation Thus it is impossible to e g add an integer with a real number The reason is that real and integer arithmetic are separate theories in Z3 A number written with a decimal point e g 2 0 will always be treated as a double If a number is written as an integer e g 2 its type can be either an integer or double depending on where it is used Additionally 1 and 0 can also be booleans If VerSAA complains about typing problems it might be because it cannot determine the correct type of the numbers involved This can be a problem especially in functional blocks if parameters are given as numeric values One suggestion is to use the the type casting function e g int32 to cast an expression to the desired type However this might affect negatively on the performance of Z3 but it seems to work well Prefer to use parameters declared in contracts or in the Matlab workspace as parameters to blocks instead of numeric values Then the type and di mension is given explicitly which makes the inference more accurate Also if parameters are set in the Matlab workspace
32. t k gt a ind X lt a j end The contract first gives the types of the inputs and outputs Here N must be given a value in the base workspace of Matlab in order for the type inference to infer dimensions The type of indices in matrices is int32 The first postcondition states that the index 7 is within matrix bounds the second states that all the elements in the vector a are greater or equal than the element at position i and the third one states that v is equal to the smallest element The lt works elementwise on the vector a and the functions all and any are generalised AND and OR respectively Using the builtin Matlab functions it is possible to write very compact specifications The tool can also expand these definitions and the verification can therefore be very efficient The invariant is then needed to prove the postcondition Recall that k is the automatically generated loop index We need to state explicitly that k is within matrix bounds Then we also need to state that the memory ind X in the delay block ind in the diagram which is used to stored the minimum found so far is within matrix bounds Finally we need to state that ind X contains the minimum found in vector a up to k 6 4 Examples involving embedded Matlab VerSAA can also be used to verify programs written in a subset of Embedded Matlab This features is mostly aimed at giving a simple environment to try out verification of matrix manipulations but it can be us
33. ther cases this is an abstraction The abstraction is adequate for the discrete parts of models with even continuous time behaviour When verifying Simulink models we are interested in showing that the ob servable behaviour does not violate some desirable property P which is here described by contracts A Simulink model can be considered a labelled transition system with state s built from the block memories as well as transitions labelled by port values p Figure 3 illustrates the situation Here s represents a value on the internal state while p represents a value on the ports Consider the property P stating that the state s is either s or s3 P s s V s 83 We can easily see that a state violating this property is not reachable from the initial state There are two approaches to verify that property P holds 1 We can compute all states reachable from an initial state s and check that we will never reach a state s where P does not hold 2 We can prove this fact inductively We show that any state s where P holds then P will hold again after any transition from s Then we also need to show that the initial state satisfies P In VerSAA approach 2 is used The advantages of this approach is that given a suitable P a suitable invariant we can check the property one transition model execution at the time This leads to potentially better scalability than in approach 1 The disadvantage is that a suitable P that enables the pr
34. ument are all examples of this type of function The second approach is enabled with the parameter expand to VerSAA The matrix operators are expanded in such a manner that Z3 only deals with scalar operators and functions This is possible since the size of all data is static and known This also keeps the used subset of the array theory decidable This will work well for relatively small matrices and vectors However this does not scale to very large matrices and vectors since the expanded formulas become too large VerSAA can handle the most common element wise operators and functions It can also do matrix multiplication and knows the functions e g zeros ones size length and transpose A more detailed list of supported functions and blocks can be found at the end of the document 5 3 Runtime errors Aside from checking that subsystems fullfill their contracts VerSAA will by default also check that all operations are well defined VerSAA will check that there are no over or underflows in integer calculations the standard signed and unsigned integer types are supported VerSAA will also check that all functions are used correctly That is VerSAA will check that e g there is no division by zero square root is not taken of a negative number and that exponentiation returns a real number Integers are used to index matrices VerSAA will also check that all matrix accesses are within matrix bounds The software in control systems is
35. x lt 0 then 1 else 1 end end Va t square x x x Va t x gt 0 gt sqrt x sart x x Va t 1 lt sin x A sin x lt 1 Va t 1 lt cos x A cos x lt 1 Uninterpreted function Supported by Z3 Vz t y t z t saturate x y z if x lt y then y else if z lt x thenz else x end end Built into Z3 to convert integers to reals Built into Z3 to convert reals to integers There are also functions to_int32 etc for converting to particular integer types Converts a double to the given integer type XX Converts a double to the given unsigned integer type XX Va double isinteger x lt a to_real to_int x bool2real True 1 0 A bool2real False 0 0 Va double real2bool x a 4 0 0 Returns the size of the argument as a two element vector Returns the length of the argument Returns a matrix filled with zeros The arguments must be constants Returns a matrix filled with ones The arguments must be constants Generalised AND that collapses a matrix Generalised OR that collapses a matrix Sum of one argument that collapses a matrix Product of one argument that collapses a matrix Min and Max of one argument that collapses a matrix Transpose of a matrix Va t x gt 0 gt factorial a x x factorial x 1 factorial 0 1 Va t x gt 0 gt sum_up x x sum_up a 1 sum_up 0 0 vectors is not supported The transpose operator cannot be used since it is
Download Pdf Manuals
Related Search