OCRA: Othello Contracts Refinement Analysis Version 1.3
Contents
1. term set term in term set membership cast operators wordl term boolean to unsigned word 1 conversion bool term toint T term swconst term integer to signed word constant conversion uwconst term integer to unsigned word constant conversion signed term unsigned word to signed word conversion unsigned term signed word to signed word conversion floor term relational_op l lt gt lt gt where e constant is a constant number e variable is a string B Abstract syntax and semantics B 1 Abstract syntax and semantics of HRELTL constraints B 1 1 Abstract syntax The logic underlying Othello constraints is called HRELTL HRELTL is built over a set of basic atoms that are real arithmetic predicates over V U NEXT V or over V UDER V where V is a set of variables NEXT V the set of next variables and DER V the set of derivatives The set PRED is defined as the set of linear arithmetic predicates in one of the following forms do 4 01 agg anUn 0 where v1 Un V ao an are constants and lt gt lt gt 4 A ao ai dx 0 where v Vo ao a are arithmetic predicates over variables in Vp and lt gt lt gt 4 The HRELTL is defined as the extension of LTL defined with the following rules if p PRED 6 and da are HRE2. CONSTRAINT always m request implies time until d request lt 3 CONSTRAINT always d alarm implies time until m in_alarm lt 3 CONTRACT alarm REFINEDBY d alarm m alarm m request CONSISTENCY NAME cl example3 alarm ASSUMPTION d alarm ASSUMPTION m request ASSUMPTION POSSIBILITY NAME pl example3 alarm GUARANTEE GIVEN d alarm ASSUMPTION m request ASSUMPTION ENTAILMENT NAME el m request GUARANTEE BY m request ASSUMPTION COMPONENT Device INTERFACE INPUT PORT x real INPUT PORT request event OUTPUT PORT alarm event PARAMETER threshold real CONTRACT alarm assume true guarantee always request and x lt threshold implies time until alarm lt 1 COMPONENT Monitor INTERFACE INPUT PORT alarm event INPUT PORT in_alarm event OUTPUT PORT request event OUTPUT PORT out_alarm event PARAMETER period real CONTRACT request assume true guarantee time until request lt period and always request implies then time until request lt period CONTRACT alarm assume true guarantee always in_alarm implies time _ until out_alarm lt 1 Figure 3 More complex OSS example Constraints may be useful to model special kind of connections such lossy channels or delays see the example in Figure 3 Remark 3 Also in this case the use of constraint may be avoided by introducing a component implementing the special connection see also Remarks 1 and 2 2 4 4 Validation Properties
3. Finally if option s is given a summary of the checks is provided hiding the formula s and description of the trace s At the moment the command can be used only for discrete time Command Options h Shows a brief description of the available options i file Reads the OSS specification If not specified the command reads from standard input a string Force algorithm type Valid values are bmc bdd ic3 auto default auto w The whole architecture is considered for the checks P name Checks only the validation property with the given name s Prints summary of the results ocra_check receptiveness Verifies if an SMV model is compatible with every Command environment satisfying the assumption of the contracts ocra_check_receptiveness I lt file gt h i lt file gt c lt name gt Given a finite state machine modeled in the SMV language and an Othello System Specification verifies if the machine is compatible with every environment satisfying the assumption of the contracts defined in the OSS At the moment the command can be used only with propositional models Command Options I file Reads the SMV specification h Shows a brief description of the available options i file Reads the OSS specification If not specified the command reads from standard input c string Specify the component to be checked ocra_check_composite_impl Check the system implementation compositionally Command or mo
4. h i lt file gt L m lt file gt o lt file gt Given an OSS specification a set of SMV files and a configuration file with a map between component names and the smv file representing their implementation outputs a single SMV file for the system implementation 14 It requires ocra_discrete_time to be enabled The configuration file looks like this Hydraulic Hydraulic smv Select_Switch Select_Switch smv subBSCU subBSCU smv That is a line for each space separeted association Command Options h Shows a brief description of the available options i file Reads the OSS specification If not specified the command reads from standard input L Disable printing of the contracts default enabled m file Reads the file with the map component name component smv imple mentation file o file Outputs the system implementation on file If not specified it prints to standard output ocra_check_consistency Check if the contracts of the whole specification are Command satisfiable ocra_check_consistency h i lt file gt j By default it checks every assertion assumption and guarantee for being consistent that is satisfiable Alter natively if the option j is given it performs richer checks e For each contract it checks consistency of the conjunction of its assumption and guarantee Notice that this check subsumes the one by default e For each composite component C checks consistency a
5. 5 time units B 2 Abstract syntax and semantics of the system specification A component S is described with a set Vg of ports which are the variables representing the relevant information of the component that are visible from outside it An implementation of a component S is defined as a subset of traces over Vs i e a subset of Ily An environment of S is also defined as a subset of IIy since Vg are the the variables at the interface of S A connection y over a set Sy of components defines the possible interaction of the components The semantics gt of a connection is defined as a subset of traces over Uses Vs i e y Mses Vs A decomposition of a component S is is pair p Subp Yp where e Sub S is a set of subcomponents such that Sub S 0 and S Sub S e y S is a connection over SP U Sub S The implementation of a decomposed component S consists of the composition of the implementations of its sub components Sub S Namely it is given by all the traces that are compatible with the subcomponents and their connection Formally if for every S Sub S Ig is the implementation of S the implementation Ig of S induced by the decomposition p is defined as r Ily there exists 7g Is for every S Sub S such that Tx Sgesu s TS l1p 5 Similarly the environment of a subcomponent U Sub S is composed by the environment of S and by the sibling subcomponents of S Formally if
6. A good condition will always hold typically the negation of condition represents some bad state always condition It is equivalent to the CESAR pattern F3 P03 Bounded Delay Each time a certain event has occurred another event will occur within a minimum delay and a maximum delay Very useful to express reactions to signals e g a safe state is entered each time an error has occurred always eventl implies time_until event2 gt interval_lower_bound and time_until event2 lt interval_upper_bound It is equivalent to the CESAR pattern R3 Delay between event and event2 within interval P04 Assured Reaction If a certain event has occurred another event will eventually occur Used in discrete time models always eventl implies not in the future event2 32 Analogue to the CESAR pattern Fl whenever eventl occurs event2 does not occur s P05 Timed Reaction Equivalent to Bounded Delay with 0 as lower bound listed here because it is commonly needed always eventl implies not time_until event2 lt interval_upper_bound Analogue to CESAR pattern F1 Combination of patterns Several times there will be the need to use more than one pattern in the same assertion For achieving this just connect them together through conjuction or disjunction patternl and or pattern2 and or patternN The following provides a reference sheet P01 Initial condition condition P02 Invarian
7. S 4 E Ports A A be oP ae 4 232 Parameters aa wre ald Bai wd a ria eee elas Ges 5 2 333 OperatiOns ore A a Pie ee RBA ke de E Peck Bay ee he bs Bard pie ee Seok Re a 5 23 4 Defines e rs y aoe es a eh Dee Me dee a ee ae a eet eee 2d 5 AS 0 65 8 es ee EAS amp eR call Ot Pee bit Ss we A eee SAEs 5 2 4 Refinement 222 404 2224 2 a E a ee ed ee Dees Ee Eee Ce eee Be R 5 24 1 lt Subcomponetts s e 664 055 bo See tee ee SAS GE AEE GY ea SSS 5 DA Ze ACONDECHONS ic ES A A e a a BGs EO ee A 6 DAA Gonstans n dic AP AH a a Beek ee A ita hg Dede ek A tg an GAENE E 6 2 4 4 Validation Properties ee 7 2 4 5 Asynchronous vs Synchronous Refinement 0 00 200 00 8 2 4 6 Contracts tefinement iio e ee lA ee we ee Ge SR Ae OG amp 8 2 5 Constraint languages road ee se oe Dee ee aoe Gb et ee eee ee 8 3 Verification of Contracts Refinement 9 4 Integration with NUXMV for Compositional Modeling and Verification 10 For a bug report a feature request or other suggestions please send email to ocra list fbk eu Advanced features 5 1 Verification of Receptiveness 5 2 Contract based Safety Analysis Interactive Commands of OCRA OCRA Command Line Options Concrete syntax A l Othello System Specification A 2 Othello Port Types o o ALZA Boolean a RA A 2 2 Enumeration Types A23 Word bit Se a ee a med t ADA Interer
8. SUB ai A SUB b B CONNECTION b in_data in_data a out_data CONNECTION positive b out_data gt 0 CONTRACT positive REFINEDBY a positive b past COMPONENT A INTERFACE OUTPUT PORT out_data real CONTRACT positive assume true guarantee always out_data gt 0 COMPONENT B INTERFACE INPUT PORT in_data real OUTPUT PORT out_data real CONTRACT past assume true guarantee always out_data lt 0 implies in the past in_data lt 0 Figure 2 Example with arithmetic expressions in the connections 2 4 2 Connections The component refinement contains a possibly empty set of connections Each connection connects the output of the component or the input of the subcomponents to an expression over the inputs of the component and the outputs of the subcomponents The connection is introduced with the keyword CONNECTION followed by the connected port and the expression The ports of subcomponents are referred to with the the dot notation name of the subcomponent followed by followed by the name of the port The type of the port and the expression must be the same So if the connected port is real then also the expression must be a real expression see the example in Figure 2 Remark 1 The presence of Boolean or arithmetic connectors in the connection may be seen as not a principled design choice because it hides a component that implements such connector OCRA supports it for flexibility but the user should
9. The component refinement contains a possibly empty set of validation properties on a contract refinement There are three types of validation properties that can be defined consistency possibility and entailment In their definitions formula ids are used to make reference to assumption guarantee and norm guarantee of the contracts of components A formula id is made up of a component name a contract name and one of the keyword ASSUMPTION GUARANTEE or NORM_GUARANTEE These three parts are separated using the dot notation see below an example Let us now explain the three type of validation properties 3Norm guarantee is defined as A gt G where A is the assumption and G is the guarantee of a given contract e Consistency this type of validation property aims at formally verifying the absence of logical contradictions of a given subset of properties assumption guarantee and norm guarantee of the contracts on a refined component and its subcomponents It is possible to define a consistency property in the following form CONSISTENCY NAME name propo propn Where propo prop is a list of formula ids e Possibility this kind of validation property allows to verify whether a property is consistent with a set of other properties specified in the contracts It is possible to define a possibility property in the following form POSSIBILITY NAME name propo GIVEN prop prop where propo can be a formula or a formula i
10. ii ahd a ele Ae ae eS AL Realo is 84 ant ue Bach oe eS A 2 6 Continuous 2 00 AZT ATAN o NA NOE Ie eB A 2 8 Uninterpreted functions A 3 Othello constraints o o Abstract syntax and semantics B 1 Abstract syntax and semantics of HRELTL constraints B 1 1 Abstractsyntax 4 B 1 2 SemanticS B 1 3 Examples B 2 Abstract syntax and semantics of the system specification Patterns 12 12 12 13 24 26 26 27 27 27 27 27 27 27 27 28 28 29 29 29 30 31 32 1 Introduction OCRA is a tool that provides automated support for contract based design with temporal logics OCRA relies on the contract framework originally proposed in CT12 CT where assumptions and guarantees are specified as temporal formulas The main functionality of OCRA is the verification of the contract refinement OCRA checks if a given contract refinement is correct generating the corresponding set of proof obligations and checking their validity OCRA takes as input a textual description of the components interfaces and their decomposition into sub components the compo nents contracts and their refinement with the contracts of the sub components The OCRA input file also called OSS OCRA System Specification describes a tree of components given by the decomposition into sub components which represents the system architecture
11. then an error message is printed informing the user that the selected trace is finite and cannot satisfy any LTL formula Command Options h Shows a brief description of the available options 7i Forces the use of the engine for infinite domains c lt name gt Component name to be assigned to the input formula p expr Checks only the given formula expr P lt name gt Checks only the property with the given name n lt number gt Checks only the property with the given index number in the property database 1 lt loopback gt Checks the property on the trace using Loopback value This must a valid Loopback value on the given trace trace_number The ordinal identifier number of the trace to be used to check the prop erty This must be the last argument of the command ocra_compute_fault_tree Generates a hierarchical fault tree from a contract Command based system decomposition ocra_compute_fault_tree C lt string gt h i lt file gt k lt int gt a lt string gt m lt file gt x lt file gt Given a contract based decomposition it generates a heirarchical fault tree according with the approach desribed in M Bozzano A Cimatti C Mattarei and S Tonetta Formal Safety Assessment via Contract Based Design In Proceedings of ATVA 2014 Sydney Australia November 3 7 2014 The optional parameter x enables the additional fault tree computation on leaves implementations by pr
12. x e lt limit and der x lt 0 are well defined formulas Predicates can be combined with Boolean and temporal operators For example x e lt limit and der x lt 0 and always x e lt limit are well defined formulas In temporal logic a formula without temporal operators is interpreted in the initial state Thus x 0 characterizes all traces that start with a state evaluating x to 0 and then x can evolve arbitrarily Instead to express that a predicates holds along the whole evolution one may use the always operator as in always x 0 Table 1 The OTHELLO constraints language grammar constraint atom po a not constraint p constraint and constraint oro constraint or constraint ov el constraint implies constraint o gt always constraint Go never constraint Gn in the future constraint Fo constraint until constraint o Ug atom true a c TI false l term relation term tet time_until term relation term pact change port v v term t term port t v constant c term function term txt der port next port v s Another classical example of properties is the response to a certain event The formula always p implies in the future q defines the set of traces where every occurrence of p is followed by an occurrence of q Note that q may happen with a certain delay although there is no bound on such delay The formula always p implies q in
13. 4 To appear CESAR patterns http www cesarproject eu fileadmin user_upload CESAR_D_ SP2_R2 2_M2_v1 000 pdf A Cimatti M Roveri A Susi and S Tonetta Validation of Requirements for Hybrid Systems a Formal Approach ACM Trans Softw Eng Methodol 21 4 22 2012 A Cimatti M Roveri and S Tonetta Requirements Validation for Hybrid Systems In CAV pages 188 203 2009 A Cimatti and S Tonetta Contracts refinement proof system for component based embedded systems Sci Comput Program To appear A Cimatti and S Tonetta A Property Based Proof System for Contract Based Design In SEAA 2012 FoReVer project https es fbk eu index php n Projects FoReVer HyCOMP website https es fbk eu tools hycomp NuSMV3 website https es fbk eu tools nusmv3 nuXmv website https es fbk eu tools nuxXmv OCRA website https es fbk eu tools ocra A Pnueli The Temporal Logic of Programs In FOCS pages 46 57 1977 24 Saf SafeCer project http www safecer eu SPE SPEED project http www speeds eu com XSA xSAP website https es fbk eu tools xsap 25 A Concrete syntax A 1 Othello System Specification An Othello System Specification OSS is written following the grammar below in Extended Backus Naur Form Oss requirements system_comp component requirements requires discrete time requires hybrid time system_comp COMPONENT comptype system interface re
14. Es is the environment of S the environment Ey of U induced by the decomposition p of S is defined as Ty Iy there exists ms Ig for every S Subp S U and 7 Ey such that x gresus s TS E ICS A system is defined by a tree of components The root of the tree is called the system component The leafs of the tree are called atomic or basic or primitive components The tree structure is given by the decomposition of each non atomic component Thus if we consider Sub as the transitive closure of the function Sub then S Sub S for any S in the system architecture Note that we avoid to distinguish between component type and component instances to simplify the notation Actually the subcomponents of a component type may be instances of the same component type and the system is a component instance We simply see two component instances as two distinct components with the same structure and renamed ports and subcomponents Given a component S a contract for S is a pair A G of assertions over Vs representing respectively an as sumption and a guarantee for the component Let C A G be a contract of S Let I and E be respectively an implementation and an environment of S We say that J is a implementation satisfying C iff IM A G We say that E is an environment satisfying C iff E C 4 We denote with Imp C and with Env C respectively the implementations and the environments satisfying the contract C Two
15. LTL formulas e is an event lt gt lt gt 4 and c an arithmetic term then e pisa HRELTL formula e 761 61 A Q2 X 01 41 U Q2 are HRELTL formulas e gt _ e isa HRELTL formula 6 As described in CRTO09 instead of constants also discrete variables can be used but the currently used SMT solver does not support non linear constraints 29 We use standard abbreviations for V gt G F R see e g CRT09 gt corresponds to time_until never is an abbreviation for G The other abstract connectives correspond the the concrete ones used in the previous section in a straightforward way B 1 2 Semantics HRELTL formulas are interpreted with hybrid traces which are defined as follows Let V be the finite disjoint union of the sets of variables Vp with a discrete evolution and Vc with a continuous evolution A state s is an assignment to the variables of V s V R We write X for the set of states Let f R be a function describing a continuous evolution We define the projection of f over a variable v written f as f t f t v We say that a function f R gt R is piecewise analytic iff there exists a sequence of adjacent intervals Jo Ji C R and a sequence of analytic functions ho h1 such that U J R and for all N f t h t for all t J Note that if f is piecewise analytic the left and right derivatives exist in all points We denote wi
16. OCRA Othello Contracts Refinement Analysis Version 1 3 Alessandro Cimatti Michele Dorigatti Stefano Tonetta Abstract Contract based design enriches a component model with properties structured in pairs of assumptions and guar antees These properties are expressed in term of the variables at the interface of the components and specify how a component interacts with its environment the assumption is a property that must be satisfied by the environment of the component while the guarantee is a property that the component must satisfy in response Contract based design has been proposed in many methodologies for taming the complexity of embedded systems In fact contract based design enables stepwise refinement compositional verification and reuse of components OCRA Othello Contracts Refinement Analysis is a tool that provides means for checking the refinement of contracts specified in a linear time temporal logic The specification language allows to express discrete as well as metric real time constraints The underlying reasoning engine allows checking if the contract refinement is correct OCRA has been used in different projects and integrated in tools This document provides a manual on how to use OCRA specifically its input language and its commands Contents 1 Introduction 3 2 Input language 3 2 1 Components til oo ah eae eee DEE eA Skee Se Sa bs 3 2 27 Hybrids Discrete Time were 6 sae A We i A ee OO a aA 4 A E RR cae Bere
17. T PORT ib boolean INPUT PORT ie event OUTPUT PORT ob boolean OUTPUT PORT oe event PARAMETER pb boolean MODULE main VAR Sensor_inst Sensor pb ie ib VAR ib boolean IVAR ie boolean FROZENVAR pb boolean DEFINE oe Sensor_inst oe ob Sensor_inst ob MODULE Sensor pb ie ib VAR ob boolean IVAR oe boolean Figure 5 A simple OCRA component and corresponding SMV template 5 Advanced features 5 1 Verification of Receptiveness For compositionality of a component with its environment it is necessary that the component does not block inputs from the environment Since we are in the contract based framework it is sufficient to consider only environments satisfying the assumptions of the component contracts This check is performed automatically by OCRA with the command ocra_check_receptiveness However the command is limited to consider only assumptions that predicate over the input ports 5 2 Contract based Safety Analysis A specific safety analysis can be performed exploiting the contract based design and identifying the component fail ures as the failure of its implementation in satisfying the contract When the component is composite its failure can be caused by the failure of one or more subcomponents and or the failure of the environment in satisfying the as sumption This dependency can be automatically computed based on the contract refinement The OCRA command ocra_c
18. The contracts are specified in Othello CRST12 a human readable language which can be mapped to temporal formulas in the HRELTL CRTO09 and thus represent sets of hybrid traces The contract refinement is however independent from the nature of the traces and OCRA provides an option to interpret the contracts over discrete time traces restricting the input to forbid continuous ports and allow LTL Pnu77 contracts only In order to prove the validity of the proof obligations deriving from contract refinement OCRA interacts with NuSMV3 NuS a framework that includes nuXmv nuX HyCOMP HyC and xSAP XSA NUSMV3 provides the functionality to either prove that the formulas are valid or to find counterexamples which can be inspected by the user in order to find the bugs in the contract refinement When the contracts are written in the standard discrete time LTL to prove or disprove the validity of the proof obligations the BDD based engine is used In the general case of HRELTL reasoning relies on Satisfiability Modulo Theory SMT Since logical entailment for HRELTL is undecidable bounded model checking techniques are used to find counterexamples to the contract refinement CRT09 CT 12 OCRA has been developed within the European project SafeCer Saf focusing on the compositional certification of embedded systems The tool is publicly available OCR 2 Input language 2 1 Components The main input of OCRA is a textual specification o
19. aer are interpreted over hybrid traces as follows e f I i Hp Peurr iff for all t L Peurr evaluates to true when v is equal to f t denoted with f t Ep p e f I i Hp Pnewt iff there is a discrete step between i and i 1 i e I Ii41 t t and peat evaluates to true when v is equal to f t and NEXT v to f t denoted with f t fizi t Ep Pnezrt e f I i Hp Paer iff for all t I Paer evaluates to true both when vis equal to f t and DER v to fe t and when v is equal to f t and DER v to f t _ denoted with f t fi t Ep Paer and fi t fi t _ Ep Paer when f t is defined this means that f t fi t Ep Paer Finally we can define the semantics of HRELTL i pitt F T i Fp p iF ab iff F T i Kd i H OA Diff f T i oand f T i H Y 1 X iff there is a discrete step ati J 1 41 and f T i 1 E 9 30 e f 1 9 U y iff for some j gt i f I j H wand forall i lt k lt j f TD k H d e f I i H gt ne iff for some j gt i I Ij t t and f I j pand forall i lt k lt j f D k Ao and for all t L t t c B 1 3 Examples The following formulas are examples of expressions with time until G p gt gt lt 10q always the maximum delay between p and the next q is 10 time units gt gt 5p A G p gt D 1o0p p happens exactly every 10 time units after an initial offset of
20. ame It is allowed to insert several options per category Command Options h Shows a brief description of the available options v Verbosely prints formula contents c lt name gt Prints out the properties of component named name a Prints only assumption properties g Prints only guarantee properties q Prints only validation properties Prints only proof obligation properties Prints only those properties found to be OK f Prints only those properties found to be NOT OK n idx Prints out the property numbered idx P lt name gt Prints out the property named name S Prints the number of stored properties ocra_check ltlspec_on trace Checks whether a property is satisfied on a trace Command ocra_check_ltlspec_on_trace h 1 n number P lt name gt c lt name gt p expr 1 loopback trace_number Checks whether a property is satisfied on a given trace The problem generated can be checked using SAT SMT backend Option i forces the use of the engine for infinite domains In case the user does not provide this option a SAT solver is called by default for checking the problem generated if only the formula and trace does not contain infinite precision variables Otherwise a SMT solver will be called for solving the problem generated We take into account that each OCRA trace may correspond to an infinite number of traces due to the possible presence of more than one loopback
21. andard input 1 lt int gt bound of K Liveness default 10 c string Specify the component to be checked k string Using bmc algorithm set the bound on length of path default 10 Us ing ic3 or kzeno set the bound of underlying IC3 default 10 a string Force algorithm type Valid values are bmc bdd ic3 auto default auto f string Selects output format Valid values are text xml default text o lt file gt Set the output file default stdout ocra_check_syntax Parses an OSS specification and type checks it Command ocra_check_syntax i lt file gt p lt string gt h C It checks the syntax of a model Command Options h Shows a brief description of the available options i file Reads the OSS specification If not specified the command reads from standard input p lt string gt Read the specification from a string E Consider the specification as an assertion default no rather than a whole OCRA system specification Equivalent to deprecated c go_ocra Parses an OSS specification and type checks it Command go ocra h i lt file gt Parses the model and performs syntactic checks over it Command Options h Shows a brief description of the available options i file Reads the OSS specification If not specified the command reads from standard input ocra_print_system implementation Compute and prints a system implementa Command tion ocra_print_system_implementation
22. bleau are not supported are not supported with the bmc engine with discrete time interpretation Command Options C lt string gt Fale k int a string Check just the specified contract rather than all of them Shows a brief description of the available options Reads the OSS specification If not specified the command reads from standard input Set the BMC length Force algorithm type Valid values are bmc bdd ic3 auto default auto f string Selects output format Valid values are text xml default text o lt file gt Set the output file default stdout 5 Prints summary of the results ocra check implementation Verifies if an SMV model satisfies the contracts de Command fined in the OSS model ocra_check_implementation I lt file gt C lt string gt h i lt file gt c lt name gt k lt int gt l lt int gt Ta lt string gt f text xml o lt file gt Given a finite state machine modeled in the SMV language and an Othello System Specification verifies if the machine satisfies the contracts defined in the OSS At the moment the command can be used only with propositional models Command Options I file C lt string gt Reads the SMV specification Check just the specified contract rather than all of them 13 sh Shows a brief description of the available options i file Reads the OSS specification If not specified the command reads from st
23. consider the alternative model where additional components are introduced and all connections are atomic just connecting one port to another port Remark 2 Jn a principled design every output port of a refined component and every input port of its subcomponents should be connected by a connection If not such port is called dangling OCRA warns the user about the presence of such ports but they are supported The semantics of dangling ports is that their value is non deterministically chosen Note that the same behavior can be obtained by adding a subcomponent that generates such non deterministic value 2 4 3 Constraints The component refinement contains a possibly empty set of temporal constraints see also Section 2 5 on the ports of the component and the ports of the subcomponents Such constraints are introduced with the CONSTRAINT In the earlier version of the language connections were named DEFINE This is no more supported COMPONENT example3 system INTERFACE INPUT PORT x real OUTPUT PORT alarm event PARAMETER min_period real PARAMETER threshold real CONTRACT alarm assume always change x implies then time_until change x gt min_period guarantee always x lt threshold implies time until alarm lt 10 REFINEMENT SUB d Device SUB m Monitor CONNECTION d x x CONNECTION alarm m out_alarm CONNECTION m period min_period lt 2 min_period 2 CONNECTION d threshold threshold
24. contracts C and C are equivalent denoted with C C iff they have the same implementations and environments i e iff Imp C Imp C and Env C Env C Contracts are used to specify the assumptions and guarantees of components in a system architecture We denote with S the contracts of the component S Since the decomposition of a component S into subcomponents induces a composite implementation of S and composite environment for the subcomponents it is necessary to prove that the decomposition is correct with regards to the contracts In particular it is necessary to prove that the composite implementation of S satisfies the guarantee of 31 S s contracts and that the composite environment of each subcomponent U satisfies the assumptions of U s contracts We perform this verification compositionally only reasoning with the contracts of the subcomponent independently from the specific implementation of the subcomponents or specific environment of the composite component Given a component Sanda decomposition p Sub y a set of contracts C E Use sus ES is a refinement of C written C lt C iff the following conditions hold 1 for any implementation J of S induced by the implementations 15 s esu s of the sub components of S and the decomposition p if for all S Sub S for all C S NC Ig Imp C then I Imp C G e the correct implementations of the sub contracts form a correct im
25. d Negative numbers can be used to denote right to left indexes from the last step Omitting this parameter causes the entire suffix of the trace to be printed A Prints the trace s using a rewriting mapping for all symbols ocra show property Shows the currently stored properties in an ocra session Command ocra show property h v c lt name gt a g q r s t n idx P lt name gt Shows the properties currently stored in the list of properties This list is initialized with the properties present in the input file if any then all of the properties added by the user with the basic command ocra check syntax or with any command which requires as input an OSS specification Generally three types of properties are distinguished contracts validation props and proof obligations In the last case the proof obligations are only added to the list of properties through the command ocra_check_refinement For every property the following informations are displayed e the identifier of the property a progressive number e the property name e the property formula e the category ASSUMPTION_PROP GUARANTEE_PROP CONSISTENCY _PROP POSSIBILITY _PROP ENTAILMENT_PROP PROOF_OBLIG_PROP and TRACE PROP the status of the property OK NOT OK N A e if the formula has been found to be false true the index number of the corresponding counterexample witness trace e the list of traces i
26. d and prop prop is a list of formula ids e Entailment this type of validation property aims at verifying whether an expected property is implied by a set of other properties specified in the contracts It is possible to define a possibility property in the form ENTAILMENT NAME name propo BY prop prop where propo can be a formula or a formula id and prop prop is a list of formula ids As we mentioned above a formula id is made up of a component name a contract name and one of the keyword ASSUMPTION GUARANTEE or NORM_GUARANTEE These three parts are separated using the dot notation For example the formula id corresponding to the assumption of the contract alarm on component example3 in Figure 3 is denoted as example3 alarm ASSUMPTION We remark that formula ids used in the definition of any validation properties can only make reference to contracts on the component where is defined the validation property and its subcomponents 2 4 5 Asynchronous vs Synchronous Refinement The semantics of the composition of subcomponents is synchronous This means that subcomponents progress si multaneously At every discrete step or time evolution every component behaves as specified by the contracts It is possible to specify an asynchronous composition by using the keyword ASYNC in front of the keyword REFINEMENT In this case at every discrete step each component either behaves as specified by the contracts or stutters The r
27. d that the property is satisfied on each one e the list of traces id that the property is not satisfied on each one Each property has a name associated except for property with category TRACE_PROP see command ocra_check_lt1lspec_on_trace Validation properties are the only ones that contain a name by definition On the other hand for each contract the name for its assumption and guarantee is defined as follows lt component gt lt contract gt ASSUMPTION GUARANTEE Finally for each proof obligation its name is defined as follows 21 lt component gt lt contract gt _ implenv _ lt subcontract gt Where e component is the name of the refined component e contract is the name of the refined contract e imp or env stands for the type of the check that is implementation or environment e subcontract present only for the environment check is the name of a contract belonging to the refinement of the contract under checking By default all the properties currently stored in the list of properties are shown without printing the formula contents The option v enable the visualization of the formulas Specifying the suitable options properties with a certain category and or of a certain status OK or NOT OK or with a given identifier or with a given name it is possible to let the system show a restricted set of properties Moreover it is possible to show all properties of a given component n
28. declares a function with two integer arguments and an integer return value PARAMETER f integer x integer gt integer In contracts function will be referenced through calls with the standard syntax guarantee always f 0 0 gt 0 2 3 3 Operations A special kind of port is called operation A component can provide an operation or require it from another one Operations can be seen as a collection of ports if an operation is declared in a component in the way shown below PROVIDED OPERATION PORT P a boolean b real boolean several ports are implicit declared and can be referenced INPUT P_call event the event corresponding to the call of the operation INPUT P_a_param boolean the first parameter INPUT P_b_param real the second parameter OUTPUT P_ret event the event corresponding to the operation returning OUTPUT P_ret_value boolean the return value Therefore the form of an operation is much like a function in a traditional programming language However there 1s no semantic constraints on the implicit ports A specific semantics should be enforce by means of constraints If no return value port is declared if the return type of the operation is void As for the other ports if a component is refined in subcomponents it is possible to define the connections between the operations 2 3 4 Defines A define is a kind of macro Every time a define is met in expressions it i
29. ela tionship between the stuttering of one component and the other events must be specified with a CONSTRAINT using the implicit event stutter For example a constraint may force a component to stutter when the other component it is performing an event See the examples in the distribution of the tool By default no fairness is introduced to avoid endless stuttering of a component By setting the option ocra_async fairness the tool will introduce such constraint 2 4 6 Contracts refinement In the component refinement each contract present in the component interface should be refined by some contracts of the subcomponents This relationship is introduced with the keyword REFINEDBY preceded by the name of the refined contract followed by a list of contracts of the subcomponents These are referred to with the the dot notation name of the subcomponent followed by followed by the name of the contract 2 5 Constraint language OCRA input language uses OTHELLO CRST12 to specify contracts In the discrete time case it coincides with LTL and is interpreted over discrete traces The relevant syntax of OTHELLO has been summarized in Table together with the corresponding mathematical formulation in HRELTL see Section B for a formal definition of syntax and semantics In case of discrete time der and time_until are not allowed Basic formulas are defined with linear arithmetic predicates over the variables or their derivatives For exam ples
30. elay defines the set of hybrid traces where p is always followed by q in less than max_delay time units 3 Verification of Contracts Refinement The contract refinements specified in the OSS be seen as a set of proof claims that are resolved by the tool The claim say 1 that if the subcomponents satisfy their contracts then also the composite component satisfies its contracts and 2 that if the subcomponents satisfy their contracts and the environment of the composite component satisfies the related assumptions then also the assumptions of each subcomponents are satisfied The OCRA command to check the refinement of contracts is ocra_check_refinement See Section 6 for a complete description of options The command internally processes the input generates the proof obligations corre sponding to the proof claims and check their validity It reports the results to standard output detailing for each proof claim if the claim is correct and if not it produces a counterexample trace witnessing that the claim is wrong A typical usage of the tool is the following First the user writes the OSS in a textual file The typical suf fix used for these files is oss for example examplel oss Emacs users can use the OCRA mode for syn tax highlighting see ocra mode el file provided with the tool distribution Second OCRA must be run in interactive mode with the command ocra int Before checking the refinement the user may check the syn tax of the in
31. es currently stored in system memory if any By default it shows the last generated trace if any Optional trace number can be followed by two indexes from_state to_state denoting a trace slice Thus it is possible to require printout only of an arbitrary fragment of the trace this can be helpful when inspecting very big traces Moreover the trace descrition also shows information of the component where was generated the trace Command Options h Shows a brief description of the available options v Verbosely prints traces content all state ports input output ports and parameters otherwise it prints out only the variables that have changed their value from previous state This option only applies when the Basic Trace Explainer plugin is used to display the trace t Prints only the total number of currently stored traces a Prints all the currently stored traces m Pipes the output through the program specified by the PAGER shell vari able if defined else through the UNIX command more 20 o output file Writes the output generated by the command to out put file trace_number The ordinal identifier number of the trace to be printed Omitting the trace number causes the most recently generated trace to be printed from_step The number of the first step of the trace to be printed Negative numbers can be used to denote right to left indexes from the last step to_step The number of the trace to be printe
32. f a system architecture and the related contract refinement The format of this input is the OCRA System Specification OSS which contains the specification of components their ports and contracts and their decomposition Each component specification starts with the keyword COMPONENT and ends with the following COMPONENT or with the end of the input For example the OSS shown in Figure 1 contains three component specifications Each component specification contains a name an interface part introduced with the INTERFACE and option ally a refinement part introduced with the keyword REFINEMENT A component without refinement is called a leaf component In the interface part the ports the parameters and the contracts are declared In the refinement part the subcomponents are declared and the connections and constraints among the ports of the component and subcompo nents are specified Finally still in the refinement part the refinement of the component contracts is also specified In the following section we detail the syntax of these elements One and only one of the component specifications is tagged with the keyword system We refer to this compo nent as the system component The system architecture is a tree of component instances where the root is an instance of the system component and each node is either an instance of a leaf component and has no children or has as children the instances specified as subcomponents in the refinement T
33. finement component COMPONENT comptype interface refinement interface INTERFACE var contract definex refinement ASYNC REFINEMENT subcomponent connection refinedby valid_prop var port parameter operation port IN OUT PORT name type parameter PARAMETER name type euf operation PROVIDED REQUIRED OPERATION PORT name op parameters type void op_parameter IN OUT name type define DEFINE name constraint type boolean integer real continuous event number name enumeration number number range unsigned signed word number euf euf_subtype euf_subtype gt euf_subtype euf_subtype boolean real integer contract CONTRACT name assume constraint guarantee constraint subcomponent SUB name comptype connection CONNECTION name constraint formula CONSTRAINT constraint refinedby CONTRACT name REFINEDBY contr_id contr_id name name valid_prop CONSISTENCY NAME name formula_id POSSIBILITY NAME name formula_id contrain GIVEN formula_id ENTAILMENT NAME name formula_id contrain BY formula_id formula_id name name ASSUMPTION GUARANTEE NORM_GUARANTEE where e name is a string e there cannot be two co
34. he system architecture of the example in Figure 1 has three nodes if simple_instance is the name of the root then simple_instance a and then simple_instance b are the leaves The OCRA data types and operators are based on the NUXMV input language See https es fbk eu tools nuxmv downloads nuxmv user manual pdf for a detailed description COMPONENT examplel system INTERFACE INPUT PORT in_data boolean OUTPUT PORT out_data boolean CONTRACT reaction assume in the future in_data guarantee always in_data implies in the future out_data REFINEMENT SUB aj Aj SUB b B CONNECTION a in_data in_data CONNECTION b in_data a out_data CONNECTION out_data b out_data CONTRACT reaction REFINEDBY a reaction b pass COMPONENT A INTERFACE INPUT PORT in_data boolean OUTPUT PORT out_data boolean CONTRACT reaction assume in the future in_data guarantee always in_data implies in the future out_data COMPONENT B INTERFACE INPUT PORT in_data boolean OUTPUT PORT out_data boolean CONTRACT pass assume true guarantee always in_data implies out_data j Figure 1 Simple OSS example 2 2 Hybrid vs Discrete Time The semantics of components is defined in terms of traces see Section B for a formal definition Traces may be discrete where the model of time is the set of natural numbers or hybrid which combines discrete changes with con tinuous evolution of time the time model in this case i
35. integer type is the set of integers Note that the use of ports with integer type requires the usage of infinite state model checking algorithms A 2 5 Real The domain of the real type is the set of real numbers Note that the use of ports with real type requires the usage of infinite state model checking algorithms A 2 6 Continuous The domain of the continuous type is the set of continuous and differentiable functions They are used to represent a value that is a continuous function of time Note that the use of ports with continuous type requires the usage of infinite state model checking algorithms and is available only for the hybrid time mode of OCRA A 2 7 Array Arrays are declared with a lower and upper bound for the index and the type of the elements in the array For example array 0 3 of boolean array 10 20 of OK y z 27 array 1 8 of array 1 2 of unsigned word 5 The type array 1 8 of array 1 2 of unsigned word 5 means an array of 8 elements from 1 to 8 each of which is an array of 4 elements from 1 to 2 that are 5 bit long unsigned words Array subtype is the immediate subtype of an array type For example subtype of array 1 8 of array 1 2 of unsigned word 5 is array 1 2 of unsigned word 5 which has its own subtype unsigned word 5 Expression of array type can be constructed with variables of array type Internally these arrays are treated as a set of variables A 2 8 Uninterpreted function
36. ions A 2 2 Enumeration Types An enumeration type is a type specified by full enumerations of all the values that the type comprises For example the enumeration of values may be stopped running waiting finished 2 4 2 0 FAIL 1 3 7 OK etc All elements of an enumeration have to be unique although the order of elements is not important A range of whole numbers can be declared with N M For example the following declarations are equivalent EA 2 3 4 5 A 2 3 Word The unsigned word e and signed word e types are used to model vector of bits booleans which allow bitwise logical and arithmetic operations unsigned and signed respectively These types are distinguishable by their width For example type unsigned word 3 represents vector of three bits which allows unsigned operations and type signed word 7 represents vector of seven bits which allows signed operations When values of unsigned word N are interpreted as integer numbers the bit representation used is the most popular one i e each bit represents a successive power of 2 between 0 bit number 0 and 2 1 bit number N 1 Thus unsigned word N is able to represent values from 0 to 2 1 The bit representation of signed word N type is two s complement i e negative numbers are represented by 2N minus their absolute value Thus the possible values for signed word N are from 2N 1 to 2N 1 1 A 2 4 Integer The domain of the
37. mong assumption of C and assumptions and guar antees of all subcomponents Command Options Shows a brief description of the available options i file Reads the OSS specification If not specified the command reads from standard input j For each contract checks consistency of the conjunction of its assump tion and guarantee and for each composite component C checks con sistency among assumption of C and assumptions and guarantees of all subcomponents ocra_check_validation_prop Check validation properties Command ocra_check_validation_prop h i lt file gt a lt string gt w P lt string gt 15 By default it check all validation properties defined in the input specification Moreover the validation properties defined in each refined component will be performed on it and its children in isolation Alternatively if the option w is given it checks all validation properties consistency possibility and entailment considering the entire architecture In more details the user can define some constraints on the architecture for example on the input of the components like setting an input into a constant from the father refinement So enable this option w the check will consider all constrains defined on the architecture contrary to the default case We remark that the generated additional checks for the different instances in the architecture using option w are not stored in the data base of properties
38. mponents with the same name e for every component there cannot be two subcomponents with the same name e compt ype is a string that matches one of the components name e in the list of components forming the OSS there exists a component whose name is system e the relationship that links a component to its subcomponents is not circular and form a tree rooted in the system component e the constraint in the definition ofa contract inan interface must be an Othello constraint as defined above where every variable must match a variable of the interface e the constraint in the definition of a connection in the refinement of a component must be an Othello constraint as defined above where every variable must either match a port of the interface or be in the form sub var where sub matches a subcomponent s name of the refinement and var matches a variable of the interface of such subcomponent e there cannot be two validation properties with the same name 26 A 2 Othello Port Types A 2 1 Boolean The boolean type comprises symbolic values FALSE and TRUE The event type has the same domain of the boolean type The difference is that while a boolean port is evaluated in a state an event is evaluated in a transition we say that an event occurs during a transition if it is TRUE in that transition Accordingly the values of event ports are listed in a separate Transition section in the OCRA counterexamples between two State sect
39. nolithically ocra_check_composite_impl m lt file gt C lt string gt h a lt string gt f lt string gt i lt file gt k lt int gt 1 lt int L M o lt file gt R s lt file gt S lt string gt 16 It checks the correctness of the system implementation with a compositional strategy by checking 1 the contract refinement 2 the implementation of each leaf component Equivalent to issue ocra_check_refinement and ocra_check_implementation on each leaf component Alternatively if the option M is given it checks the correctness of the system implementation with a monolithic strategy It computes the system implementation out of the leaf components and the system architecture and it checks its correctness Equivalent to issue ocra_print_system_implementation and ocra_check_implementation Command Options m file Reads the file with the map component name component smv imple mentation file C lt string gt Check just the specified contract rather than all of them h Shows a brief description of the available options a string Force algorithm type Valid values are bmc bdd ic3 auto default auto f string Selects output format Valid values are text xml default text i file Reads the OSS specification If not specified the command reads from standard input k int Set the BMC length 1 lt int gt bound of K Liveness default 10 L Disable printing of the contract
40. nstraint releases constraint temporal past operators historically constraint in the past constraint previously constraint constraint Since constraint constraint triggered constraint atom TRUE FALSE term relational_op term time _ until term relational_op term term term variable constant term term term term term x term term term term mod term 5The OCRA data types and operators are based on the NUXMV input language See https es fbk eu tools nuxmv downloads nuxmv user manual pdf for a detailed description 28 term index array indexing der variable next variable function term term x function call term 2 term term compact if then else case term term esac if then else count term term x count of true boolean expressions word operators term gt gt term bit shift right term lt lt term bit shift left term term term word bits selection term term word concatenation sizeof term word size as an integer extend term term word width extension resize term term word width resize signed word N term integer to signed word conversion unsigned word N term integer to unsigned word conversion set operators term union term term
41. ompute_fault _tree produces a fault tree in which each intermediate event represents the failure of a component or its environment and is linked to a Boolean combination of other nodes the top level event is the failure of the system component while the basic events are the failures of the leaf components and the failure of the system environment see BCMT 14 for more details 12 6 Interactive Commands of OCRA ocra_check_refinement Checks the contract refinement of the OSS Command ocra_check_refinement text xml C lt string gt h i lt file gt k lt int gt a lt string gt o lt file gt s First it checks the syntax of a model In case of error a message is given Second it checks that a given system architecture is correct with respect to the specified refinement of contracts The verification guarantees that if the implementations of the leaf components are correct then for every composite component C e every contract of C is satisfied by the implementations of the subcomponents of C e every assumption of a subcomponent of C is satisfied by the implementations of the other subcomponents of C or by the environment of C If the check finds that the refinement is wrong the system gives you a counterexample In case that option s is given a summary of the checks is provided hiding the formula s and description of the trace s Currently past operators and option bmc_force_pltl_ta
42. ontract gt _ ile lt subcontract gt lt extension gt Where e model is the pathname of the input oss e component is the name of the refined component e contract is the name of the refined contract e i or e stands for the type of the check that is implementation or environment e subcontract present only for the environment check is the name of a contract belonging to the refinement of the contract under checking 19 Command Options Shows a brief description of the available options i file Reads the OSS specification If not specified the command reads from standard input o file Set base output file name ocra discrete time Environment Variable Interpret the ocra specification over discrete time Default is false specification is interpreted over hybrid time ocra make warnings errors Environment Variable Treat every warning as an error Default is false ocra_old_smv_format Environment Variable Write and read SMV models with the format used before version 1 3 0 Default is false ocra_async fairness Environment Variable Add to the specification the constraint that each subcomponent will eventually not stutter It affects only models with asynchronous refinement ocra_show traces Shows the traces generated in an ocra session Command ocra_show_traces h v t A m o output file Ta trace_number from_state to_state Shows the trac
43. oviding a fault injection xml file description Command Options C lt string gt Check just the specified contract rather than all of them f Shows a brief description of the available options i file Reads the OSS specification If not specified the command reads from standard input k lt int gt with bmc bound on length of path default 10 with ic3 or kzeno bound of underlying IC3 default 10 23 a lt string gt force algorithm type default auto Valid values are bmc bdd ic3 auto m lt file gt Set a file with the mapping OSS component SMV file Its format is OSS component namez SMV filename Equivalent to deprecated a x lt file gt XML file describing the fault extension 7 OCRA Command Line Options ocra discrete tim Enables the interpretation of the model over discrete time instead of default hybrid time The model must not contain e continuous variables e der operator e time_until operator ocra o1d smv format Write and read SMV models with the format used before version 1 3 0 ocra async fairness Add to the specification the constraint that each subcomponent will eventually not stutter It affects only models with asynchronous refinement References BCMT14 M Bozzano A Cimatti C Mattarei and S Tonetta Formal Safety Assessment via Contract Based CES CRST12 CRT09 CT CT12 FoR HyC NuS nuX OCR Pnu77 Design In ATVA 201
44. plementation of C 2 for every subcomponent S of S for every contract C S NC for any environment E of S induced by the decomposition p the environment E of S and the implementations Is 5 esuo s s Of the sub components of S if E Env C and for all S Sub S S for all C E S NC Igy Imp C then E Env C i e for each sub contract C the correct implementation of the other sub contracts and a correct environment of C form a correct environment of C C Patterns The Othello language is an expressive and complex language This can be a problem for a user non specifically trained with the formal languages On one side it is possible to write contracts that do not represent the wanted requirement On the other side it can happen to write a specification that represents a unnecessary hard satisfiability problem For this reason we list here several constraint patterns mostly inspired by the SPEED SPE and CESAR CES projects The list is the result of an analysis of the use cases developed so far both internally and with our partners in Safecer Saf and Forever FoR projects With a few exceptions all those realistic contracts can be expressed using only these patterns P01 Initial condition The condition that must hold in the initial state of the system It is a common mistake to write such constraint instead of always condition condition P02 Invariant
45. ponds to SMV variable of type X OCRA input event port corresponds to SMV input variable of type boolean 4see the nuXmv user manual https es fbk eu tools nuxmv downloads nuxmv user manual pdf 10 Modeling Verification amp validation Figure 4 Three scenarios of usage of nuXmv and OCRA in a nutshell OCRA output event port corresponds to SMV input variable of type boolean OCRA parameter of type X corresponds to SMV frozen variable of type X Note that the word input has different meanings e Since in SMV there is no distinction between input and output we use the convention that inputs correspond to variables declared outside the component module and passed to module through MODULE parameters while outputs correspond to some symbols declared insider the MODULE Main SMV module For each parameter there must be a frozen variable FROZENVAR This has to be also an actual parameter to the module instance For each input port there must be a state variable VAR This has to be an actual parameter to the module instance as well For each output port there must be a DEFINE Its body must be a symbol with the same name in the module component name There must be a single module instance of type component name Component SMV module e For each input port and parameter there must be a parameter e For each output port there must be a symbol 11 COMPONENT Sensor system INTERFACE INPU
46. put by calling ocra_check_syntax i examplel oss OCRA provides also a simple valida tion check that verifies if each constraint in the contracts is satisfiable This can be performed with the command ocra_check_consistency Finally after syntax checking and validation the user may run the actual verification with the command ocra_check_refinement The overall sequence therefore is ocra int ocra gt ocra_check_syntax i examplel oss ocra gt ocra_check_consistency ocra gt ocra_check_refinement 4 Integration with NUXMV for Compositional Modeling and Verification When considering discrete time behaviors OCRA is tightly integrated with the nuXmv model checker to model and verify behavioral models that implement the OCRA components The behavior of components can therefore described in the SMV language the input language of NuSMV and nuXmv In SMV the behavior is described by means of logical formulas that describe the initial states and the state transitions An SMV specification can be organized by modules but the language does not allow to have a component based specification with a clear definition of the component interfaces In fact in the discrete time case OCRA can be used even without contracts just to specify SMV in a component based fashion Figure 4 shows in a nutshell three different scenario of modeling and verifying SMV models in the first scenario only the SMV language and the nuXmv model checker is used in the second
47. s In OCRA it is also possible to define uninterpreted functions Only parameters can be declared with this type These functions are rigid i e their denotation does not change from two different time points These functions can be seen as parameters the denotation of the function is defined in the initial state and kept from that point on Below is reported a simple example of declaring a function funct1 that takes two reals as arguments and returns an integer and a function funct2 that takes two reals and returns an unsigned word of size 32 PARAMETER functl real real gt integer PARAMETER funct2 real real gt unsigned word 32 Note Currently in OCRA we only support a limited number of data types both as return type and as type of each argument of a function In particular the supported types are boolean real integer and word N Support for richer types e g enumeratives bouded integers and array is ongoing A 3 Othello constraints An Othello constraint is written following the grammar below in Extended Backus Naur Form constraint atom boolean operators not constraint constraint and constraint constraint or constraint constraint xor constraint constraint implies constraint constraint iff constraint temporal future operators always constraint never constraint in the future constraint then constraint constraint until constraint co
48. s So it is not possible or at least straightforward to check all of them Therefore we consider just one loopback and provide the user with the possibility to select it A expr to be checked can be specified at command line using option p This formula is added to the data base of property with the category TRACE_PROP Each property in the data base is associated with component information 1 e option c allows to the user to associate expr with the component information provided In case the user does not provide this information the component associated to expr is the component system by default 22 Alternatively options n and P can be used for checking a particular formula in the property database If neither n nor p nor P are used then each contract assumption and guarantee in the OSS specification is checked on the given trace The loopback value can be specified at command line using option 1 This must a valid Loopback value on the given trace If it is not valid then an error message is printed and also the available loopbacks are provided In case that option 1 is not used then a warning is printed and the check is performed using the first loopback found on the given trace Finally the last argument of the command is the trace number which has to correspond to a trace stored in the system memory If the trace number is omitted then an error message is printed In case that the trace has not loopbacks
49. s default enabled M Perform a monolithic verification by building the system implementation o lt file gt Set the output file default stdout R Skip the refinement check s lt file gt Set the output file for the system component default None S lt file gt Select which checks are performed on the leaves de fault implementation Valid values are full implementation none receptiveness ocra_print_implementation_template Prints the SMV templates of the leaf com Command ponents ocra_print_implementation_templat h i lt file gt L m lt file gt The purpose of this command is to aid the modelling of the implementations of the basic leaf components of a system It generates one o more SMV files each of them representing the implementation of a leaf component The generated models are templates they contain just the language of the component If m is given only the listed components are processed and the SMV files are named according to the mapping Otherwise all the leaf components are processed and the SMV files are named after the name of the components 17 The configuration file looks like this Hydraulic Hydraulic smv Select_Switch Select_Switch smv subBSCU subBSCU smv That is a line for each space separated association Command Options h Shows a brief description of the available options i file Reads the OSS specification If not specified the command reads from standard inp
50. s substituted by the expression associated with this define Therefore the type of a define is the type of the associated expression in the current context Define expressions may contain next operators normal rules apply no nested next operators A define is not a port or a parameter so it cannot be used in the left hand side of a CONNECTION 2 3 5 Contracts A component interface may contain a set of contracts Each contract is introduced with the keyword CONTRACT followed by the name of the contract and two constraints see also Section 2 5 representing an assumption and a guarantee The assumption is introduced with the keyword assume and represents a property that must be satisfied by the environment of the component The guarantee is introduced with the keyword guarantee and represents a property that must be satisfied by the implementation of the component provided that the assumption holds 2 4 Refinement 2 4 1 Subcomponents The component refinement contains a set of subcomponent declarations Each subcomponent is introduced with the keyword SUB followed by the name and the type The type must be the name of another component However the type cannot be the refined component or any ancestor in the tree structure of the system architecture COMPONENT example2 system INTERFACE INPUT PORT in_data real OUTPUT PORT positive boolean CONTRACT positive assume always in_data gt 0 guarantee always positive REFINEMENT
51. s the subset of N x R containing 0 0 and such that for all i t i t if lt 0 then t lt t The default model is hybrid In the discrete time case the language is syntactically restricted see Section 2 3 1 and 2 5 The user can require to interpret the model with discrete time by writing at the beginning of the model requires discrete time 2 3 Interface 2 3 1 Ports The component interface contains a possibly empty set of port declarations Each port is declared with the keyword PORT preceded by the direction INPUT OUTPUT and followed by the name and the type Allowed types are boolean integer real event continuous signed word unsigned word range of integers list of integers or symbolic constants In the discrete time case continuous type cannot be used 2 3 2 Parameters A component interface may contain also parameters These are introduced with the PARAMETER The type of param eters can be boolean integer real signed word unsigned word range of integers list of integers or symbolic constants and uninterpreted functions Parameters are like input port that do not change value along time The parameters of subcomponents can be set by the connection see the example in Figure 3 Therefore the same component can be instantiated with different parameters Moreover the value may depend on the parameters of the father component Parameters can be declared with the uninterpreted function type The following code
52. scenario the system architecture is specified in OSS even without contracts the behavior of the leaf component is specified in SMV OCRA generates the SMV of the system composing the leaves according to the architecture and finally nuXmv is used to verify the model as a whole in the third scenario contracts are also specified in the OSS model and OCRA is used for a composition verification In order to support this usage several commands of OCRA take as input or return as output SMV models These models represent an instantiation of the OCRA component in a free environment They contain a module correspond ing to the OCRA component and a module main instantiating the component Going to the detailed syntax other than being valid SMV models to be used with OCRA these models need to follow the syntax described below When starting to model the implementations of an OCRA specification it is possible to automatically generate the correct structure using the command ocra_print_implementation_template Figure 4 shows a simple OCRA component and the corresponding SMV template Note that OCRA version 1 2 0 and earlier used a different now deprecated syntax If needed it can be enabled with set ocra_old_smv_format General rules e Types are slightly different in OCRA and SMV so that the following correspondence must be followed OCRA input data port of type X corresponds to SMV variable of type X OCRA output data port of type X corres
53. stead forces q to happen at the instant of p The above formulas do not constrain the time model of the traces Therefore they can be interpreted either as discrete traces or as hybrid traces However the logic is suitable to characterize specific sets of hybrid traces constraining when there should be discrete events and how the continuous variables should evolve along continuous evolutions The der operator is used to specify constraints on the derivative of the continuous evolution of continuous variables For example the following OTHELLO constraint always train location lt target implies der train location gt 0 characterizes the set of hybrid traces where in all states if the train has not yet reached the target location its speed expressed as the derivative of the location is greater than or equal to zero The next operator is used to specify functional properties requiring discrete changes to variables For example we can express the property that the warning variable will change value after the train s speed passes the limit with the following constraint always speed gt limit implies in the future next warning warning The expression change x can be used instead of next x x In order to constrain the delay between two events we use the time_until operator which denotes the time that will elapse until the next occurrence of an event For example the formula always p implies time_until q lt max_d
54. t always condition P03 Bounded Delay always eventl implies time_until event2 gt interval_lower_bound and time_until event2 lt interval_upper_bound P04 Assured Reaction always eventl implies not in the future event2 P05 Timed Reaction always eventl implies not time_until event2 lt interval_upper_bound Combination of patterns patternl and or pattern2 and or patternN 7As a technical note notice that it not possible to express in Othello this CESAR pattern with a lower bound different from 0 The semantic of CESAR would be that event2 must occur during the interval and can occur before it However the current Othello language would force the event to not occur before the specified interval as in Bounded Delay 33
55. th f the derivative of a real function f with f t _ and f t the left and the right derivatives respectively of f in t Let I be an interval of R or N we denote with le T and ue T the lower and upper endpoints of J respectively We denote with R the set of non negative real numbers A hybrid trace over V is a sequence f I fo Io f1 11 f2 T2 such that for all i N e either J is an open interval I t t for some t t RF t lt 1 oris a singular interval 1 t t for some t Rt e the intervals are adjacent i e we J le Ii41 e the intervals cover Rt U y I R thus Zo 0 0 e f R gt X is a function such that for all v Vo f is continuous and piecewise analytic and for all v Vp f is constant e if L t Y then fi t fi i fit fiat We denote with PRED the set of predicates with p a generic predicate with Peurr a predicate over V only with Pnex a predicate over V and NEXT V containing at least an event variable or a next variable and with pac a predicate over V and DER V containing at least a derivative variable We denote with p the predicate obtained from p by replacing lt with gt gt with lt with and vice versa We denote with p the predicate obtained from p by substituting the top level operator with for lt gt lt gt The HRELTL is interpreted over hybrid traces The predicates pourr Pnext aNd P
56. ut L Disable printing of the contracts default enabled m file Reads the file with the map component name component smv imple mentation file ocra_write anonymized models Prints the SMV templates of the leaf compo Command nents ocra_write_anonymized_models h i lt file gt m lt file gt d lt file gt The configuration file looks like this Hydraulic Hydraulic smv Select Switch Select Switch smv subBSCU subBSCU smv That is a line for each space separated association Command Options h Shows a brief description of the available options i file Reads the OSS specification If not specified the command reads from standard input m file Reads the file with the map component name component smv imple mentation file d file Reads the file with the map component name component smv imple mentation file ocra_print_proof_obligations Prints on files the proof obligations composing the Command refinement check ocra_print_proof_obligations h i lt file gt o lt file gt It computes the proof obligations that compose the refinement check and prints them as SMV files if discrete time interpretation is selected as HRELTL files otherwise Trivial proof obligations are not printed 18 If o option is given its value is used as a prefix that together with a counter is used as filename Otherwise the filename will follow this format lt model gt _ lt component gt lt c
Download Pdf Manuals
Related Search