Formal Refinement Support
Contents
1. sec ans inc minsReq min MinInit mu X X AN ans inc minsReq We also apply the law Copy Rule from Right to Left to the body of the recursions introducing the action calls for the left hand side RunSec and for the right hand side RunMin This steps produce the following action which apart from parentheses is the same as the main action of the concrete process thus demonstrating that one is the refinement of the other sec ans inc minsReg min MinInit mu X RunMin X ans inc minsReq SecInit mu X RunSec X This example has been fully developed in the refinement plugin but no attempt was made to verify the provisos that were not discharged automatically by the refinement tool 3 2 Distributed mini Mondex Unlike the previous case study the mini Mondex example cannot be fully devel oped using the refinement plugin It is nevertheless an important case study in that it demonstrates the suitability of the refinement calculus for the verification of emergent properties 26 D33 4 Refinement Support Public COMPASS Abstract Contract Concrete transfer Spec 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 I cards 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 reqs sum cards M dom reqs subset IS Figure 9 The Mini Mondex process ref2. 1 Take the selected AST node and feed it through the Maude pretty printer visitor which converts it to the format expected by Maude http maude cs uiuc edu primer maude primer pdf Personal website http www ccse kfupm edu sa musab 48 D33 4 Refinement Support Public COMPASS 2 search for applicable laws for this node using the precondition rules which is then returned to Symphony for display in the refinement law list 3 once a law is applied apply the corresponding refinement law in Maude to get the resultant AST node The returned AST mode goes through a transformation to remove Maude specific encoding information To exemplify refinement laws in Maude we illustrate the encoding of the follow ing law combination of guards gl 92 amp A gl and 92 amp A This law simply states that two guards can be composed to produce a single guard through conjunction In Maude we implement this using the following two rewrite laws rl pre guard combination refs gl amp paren g2 amp A gt rinf guard combination Guard combination gl 92 amp A gl and g2 amp A r rl guard combination refine guard combination lt g1 amp paren g2 amp A M p gt gt lt gl and g2 amp A M p gt The first law is used to encode that the refinement is applicable for nodes of the form g1 amp g2 amp A Specifically when the
3. e an applicability condition isApplicable INode node which checks if the refinement law can be applied to the given AST node e a list of required meta variable parameters getMet as e an application method apply Map lt String INode gt metas INode node int offset which applies a refinement law under a suitable map of meta variable substitutions to a given AST node with a specified textual offset to represent any indentation of code The method returns text which can be spliced into the CML file A programmatic refinement law simply consists of a Java class that implements this interface Typically isApplicable will check if the passed AST nodes are of a particular class using instanceof and apply will manipulate the input AST node Programmatic refinement laws are useful for when a complex imperative manipulation is needed or access to data not contained in the AST fragment is required such as external AST nodes or other resources However they also require the most effort to implement as pattern matching and extraction must be written manually 4 3 Maude refinement laws 4 3 1 Introduction to Maude The Maude System is an engine for executing specifications written using rewrite logic A user typically specifies a collection of sorts term constructors equations for these terms and finally rewrite laws which specify how terms of a particular form can be rewritten to other terms Maude can then b
4. ans inc minsReg min D33 4 Refinement Support Public COMPASS AN ans inc minsReg frame wr min pre true post min frame wr sec pre true post sec mu x time gt minsReq gt ans mins gt out mins sec gt Skip tick gt MESE sec 0 amp inc gt Skip sec lt gt 0 amp Skip tod e o 7 X sec ans inc minsReg min mu X inc gt ESA minsReg gt ans min gt Skip 7 X AN ans inc minsReg One more time we apply the law Copy Rule from Left to Right to remove the calls to incSec and incMin frame wr min pre true post min 0 frame wr sec pre true post sec mu X time gt minsReq gt ans mins gt out mins sec gt Skip Il o tick gt frame wr sec post sec sec 1 mod 60 sec 0 amp inc gt Skip sec lt gt 0 amp Skip X sec ans inc minsReg min mu X inc gt frame wr min post min min 1 mod 60 minsReg gt ans min gt Skip 19 D33 4 Refinement Support Public COMPASS ans inc minsReq X se Next we apply the law Distribute hiding over sequential composition to the whole main action N D33 4 Refinement Support Public COMPASS ans inc minsReq lt Ea Now we apply the law
5. sec lt gt 0 amp Skip time gt minsReg gt ans mins gt out mins sec gt Skip RunMin inc gt incMin minsReq gt ans min gt Skip SecInit mu X RunSec X sec inc minsReg ans min MinInit mu X RunMin X linc minsReg ans end In order to verify this refinement we start from the abstract specification and as a first step add all the auxiliary actions of the concrete specification This first step does not change the meaning of the abstract specification because these new actions are not used directly or indirectly in the main action of the abstract specification 14 D33 4 Refinement Support Public COMPASS In what follows we highlight changes introduced by refinement laws in yellow and actions that must be selected for the application of laws in gray The yel low highlights refer to the laws described in the paragraph before the CML code and the gray highlights refer to selections required for the laws described in the paragraph that follows the CML code process AChronometer begin state sec RANGE min RANGE frame wr sec min pre true post sec 0 and min 0 Run tick gt incSec sec 0 ESA sec lt gt 0 amp Skip time gt out lmin sec gt Skip 15 D33 4 Refinement Support Public COMPASS e E mu x e SE x end Next we apply the law Copy Rule from Left to Rightlllto AInit Run
6. incSec and incMin in order to obtain the main action without any action calls frame wr sec min pre true post sec 0 and min 0 mu X tick gt sec lt gt 0 amp Skip time gt out min sec gt Skip X frame wr sec min pre EE post sec 0 and min 0 mu X tick gt frame wr sec post sec sec 1 mod 60 sec 0 amp frame wr min post min min 1 mod 60 sec lt gt 0 amp Skip time gt out min sec gt Skip X Next we apply the law Unit of logical And 2 to transform the precon dition of the first specification statement into a conjunction of true frame wr sec min pre true and true post sec 0 and min 0 mu X tick gt frame wr sec post sec sec 1 mod 60 sec 0 amp frame wr min post min min 1 mod 60 Tt is worth mentioning that the early application of copy rules is sometimes unnecessary from the point of view of the refinement but necessary in our case due to a limitation of the tool in the calculation of functions such as usedC that require the complete definition of the action passed as parameter 16 D33 4 Refinement Support Public COMPASS sec lt gt 0 amp Skip time gt out min sec gt Skip X This is necessary to put the action in the correct form for the application of the next law which is Specification Sequential Introd
7. sec 1 sec 0 amp inc gt Skip sec lt gt 0 amp Skip 7 X mod 60 I sec ans inc minsReq min AN ans inc minsReq mu X time gt minsReq gt ans mins gt out mins sec gt Skip 24 D33 4 Refinement Support Public COMPASS sec 0 amp inc gt Skip sec lt gt 0 amp Skip 7 X sec ans inc minsReg min frame wr min pre true post min 0 mu X inc gt frame wr min post min min 1 mod 60 minsReq gt ans min gt Skip X ans inc minsReg Finally we apply the law Copy Rule from Right to Left to the speci fication statements the first with name SecInit the second with name incSec the third with name MinInit and the fourth with name incMin au SecInit mu X time gt minsReq gt ans mins gt out mins sec gt Skip tick gt EEE sec 0 amp inc gt Skip sec lt gt 0 amp Skip 7 X sec ans inc minsReg min MinInit mu X inc gt incMin 1 minsReq gt ans min gt Skip X AN ans inc minsReq au SecInit D33 4 Refinement Support Public COMPASS mu X time gt minsReq gt ans mins gt out mins sec gt Skip HEN Eick gt meses 7 sec 0 amp inc gt Skip a sec lt gt 0 amp Skip 7 X
8. NM gt guard combination DS gt Guard combination LD gt gl g2 A gl and g2 amp A INP gt Solution 2 state 2 states 3 rewrites 2 NM gt guard weaken DS gt Guard Weakening LD gt g1 amp A g2 A provided g2 gt gl INP gt meta g2 expression No more solutions states 3 rewrites 2 We encode the AST node in Maude using the visitor and then search for possible rewrites which give refinement information In this case we get two applicable laws the first is the application of the guard combination law and the second the guard weakening law which we shortly exemplify The information output is then sent back to Symphony as a text block and assuming the first law is picked we execute it using the refine command search in ACTION REFINE refine guard combination lt nm x gt n 0 amp paren nm x lt n 5 amp Skip M b true gt gt x lt A M p gt Solution 1 state 1 states 2 rewrites 1 A gt nm x lt n 5 and nm x gt n 0 amp Skip M gt M p gt b true 50 D33 4 Refinement Support Public COMPASS No more solutions We specify the refinement law code to be executed guard combination and the AST node to refine and the result consists of the new node the meta variable map here irrelevant and the proviso of the law which in this
9. theorem proving model checking etc and therefore can be subject to rigorous analysis which would otherwise by difficult in a large dis tributed SoS A verified contract can then be refined into a collection of processes which map onto the topology of the contract As a consequence of refinement properties verified for the abstract model also hold in the concrete one Therefore we also 40 D33 4 Refinement Support Public COMPASS provide an approach for the verification of emergent properties which are speci fied as the invariants in the SoS contract 4 Technical Overview 4 1 Functionality and workflow The core of the refinement tool consists of an interface for pattern matching a fragment of the CML AST and execution of applicable laws to update the AST at this location A refinement law is essentially a functional rewrite rule over a particular kind of AST node possibly with meta variables and side conditions provisos The main control loop follows this sequence 1 select a fragment of the AST where the user has selected or placed his cur sor The AST node selected is calculated as the least common ancestor for the nodes at the beginning and end of the selection For example in Skip Stop Skip if we select between the t in Stop and the i in the second Skip then we will select node Stop Skip 2 check for applicability of all known refinement laws to this AST fragment usually via a pattern match but potent
10. This mimics as much as possible the syntax of CML as given by the Symphony tool so that applied re finements do not need much conversion We have extended this AST with further constructs from the CML language and implemented a number of syntax level functions such as the free variable function FV the written variables function wrtV and used channel function usedc both of which are required by several refinement laws for provisos For more information about side conditions in re finement laws please refer to 0106 We have also implemented some basic congruence laws for CML expressions and actions using equations which means Maude can also prove simple theorems during refinement and therefore discharge provisos Refinement laws are encoded in Maude using a pair of rewrite rules e the precondition rule which tests whether a given refinement law is appli cable and if so returns information about the law e the refinement rule which encodes the step of the refinement In Maude these are encoded using rules of the following form respectively refs A gt rinf NM DS LD INP refine NM lt A M p gt gt lt A M p gt Where A A are CML AST nodes NM DS and LD are information strings en capsulating the law name description and content INP is a set of possible input variables M M are meta variable maps p p are proviso expressions The con trol loop for Maude refinement then is
11. composition of the initialisation of sec followed by the iterative execution of RunSec and the initialisation of min followed by the iterative execution of RunMin with the channels inc minsReq and ans hidden 11 The parallel composition specifies that the left hand side can only modify the state components sec the right hand side can only modify the state component min and both sides must synchronise on the channels inc minsReq and ans This process reacts to tick or time which are both offered by the left hand side of the parallelism In the first case this action increments the components sec and if the result of the increment is zero requests through the channel inc that the 13 D33 4 Refinement Support Public COMPASS other parallel action increment min In the second case it requests through the channels minsReq and ans the current value of min and communicates it along with the value of sec through the channel out The channels inc minsReg and ans are only used for internal communications between the two parallel actions are internal and are therefore hidden process CChronometer begin state sec RANGE min RANGE actions SecInit frame wr sec pre true post sec 0 MinInit frame wr min pre true post min 0 incSec frame wr sec post sec sec 1 mod 60 incMin frame wr min post min min 1 mod 60 RunSec tick gt incSec sec 0 inc gt Skip
12. gt Figure 2 Selection of refinement perspective D33 4 Refinement Support Public COMPASS The refinement perspective consists of six areas as shown in Figure 3 CML Ex plorer CML Editor Refinement Law Details Refinement Laws CML RPO List and CML RPO Details The first two are the same as in the CML perspective The panel Refinement Laws presents the list of applicable refinement laws the Refine ment Law Details panel shows the details of the selected refinement law the CML RPO List panel lists all the proof obligations refinement provisos generated by the application of refinement laws and the RPO Details panel presents the details of a selected proof obligation Sucar aia a s a A EJ cm Explorer 3 D B testem x 6 TC Refinement Laws 3 Ein a alt 7 channels c nat Law Name Y test process test begin gt Eltest cml state Bitest cm vi nat 1 actions A truel clv gt A Refinement Law List B val x nat Stop QA B v end E CML RPO List 33 ml Nc Re Type Source Refinement Proof Obligations E Refinement Law Details 33 lt Refinement Laws gt E CML RPO Details lu Refinement Law Details RelinemantObligationa Details Writable Insert 13 4 Figure 3 Refinement perspective In order to apply a refinement law the excerpt of the specification to which the law is to be applied must be selected as shown in Figure 4 The selection algorithm chooses the least common node
13. refinement tool searches for applicable laws for a given AST node A it will ask for possible rewrites for refs A from Maude using the search command The list returned is then all possible refinements steps Application of refs returns a quadruple con sisting of the law code law name a textual description of the law and a set of meta variables which are required for the law to be applied The second law defines the actual rewrite the refinement law performs Once law with code 1 has been chosen the tool will send to Maude a request to rewrite refine l lt A M p gt where Mis a map from meta variable names to values currently either an action or expression and p is a set of provisos Maude will then construct a new AST fragment using the meta variables when necessary and a set of additional provisos required to support the law In the case of our example law no meta variables are required and no provisos so the rewrite law simply performs the node update 49 D33 4 Refinement Support Public COMPASS To illustrate these laws in action we exemplify the process in Maude The user has requested to refine the AST node x gt 0 amp x lt 5 amp Skip The first step is to search for applicable laws using the Maude search command Maude gt search refs nm x gt n 0 amp paren nm x lt n 5 Skip gt rinf NM DS LD INP Solution 1 state 1 states 2 rewrites 1
14. 1 2 amp transfer 2 tgt2 m2 gt MkTran 2 mu X i Index RecTranReg i RejTran i EffTran i X end Next by applying the copy rule to the operation calls and further simplifying the model we obtain the following actions actions RecTranReq i Index i 1 gt not hasl and i 2 gt not has2 amp pay i j 1 lt gt j n n gt 0 gt cases 1 1 gt hasl true srcl i tgtl j ml n 2 gt has2 true src2 i tgt2 j m2 n end RejTran i Index i 1 and hasl or i 2 and has2 and 1 1 and ml gt cardl or 1 2 and m2 gt card2 amp reject i gt Cases 1 1 gt hasl false 2 gt has2 false end 33 D33 4 Refinement Support Public COMPASS EffTran i Index i 1 and hasl or i 2 and has2 and 1 1 and ml lt cardl or 1 2 and m2 lt card2 amp i 1 amp transfer 1 tgt1 m1 gt cardl cardi ml cases tgtl 1 gt cardl cardi ml 2 gt card2 card ml end hasl false i 2 amp transfer 2 tgt2 m2 gt card2 card2 m2 cases tgt2 1 gt cardl cardl m2 2 gt card2 card2 m2 end has2 false mu X i Index RecTranReg i RejTran i EffTran i X end At this point we expand the external choices over the set of indices apply the copy rule to replace the calls
15. 4 Refinement Support Public COMPASS The applicable laws are then loaded onto the Refinement Laws panel and a law may be selected as shown in Figure 6 In this case the details of the law are presented in the bottom panel and the law can be applied by double clicking it In some cases application of a law may lead to a refinement proviso being raised which will be added to the refinement proviso list m 4 ara sr ey Q EJCML E Refinement EJ CML Explorer 33 E Eltesteml 3 E E Refinement Laws E O a gt channels c nat Law Name v test process test shape implicit to Explicit Recursion Eltest cml Lie une Dummy Law actions A true amp clv gt A B val x nat Stop A Biv end E CMLRPOList 3 imj Nc Re Type Source E Refinement Law Details 33 a0 N A N mu X A X E CMLRPO Details 3 Figure 6 Selection of refinement law The refined CML specification is shown in the CML Editor and further refinement laws can be applied Figure 7 In this example a refinement law is applied to make the implicit recursion in A explicit using the mu operator 3 Case Studies In this section we discuss two case studies for refinement in CML 1 Chronometer refinement This example is a simple refinement that intro duces a parallel implementation of a centralised specification Its main goal is to demonstrate the usability of the tool 2 Distributed mini Mondex The mini Monde
16. Jeremy Jacob The Certification of the Mondex Electronic Purse to ITSEC Level E6 Formal Aspects of Computing 20 1 5 19 2008 Frank Zeyda Marcel Oliveira and Ana Cavalcanti Mechanised sup port for sound refinement tactics Formal Aspects of Computing 24 1 127 160 2012 56
17. MPASS model checker Certain refinement laws are also parametric meaning the right hand side contains meta variables not mentioned in the left hand side Therefore in order to apply these laws it is necessary for the user to fill in values for the variables This being the case the tool will upon application of the law pop up a series of dialog boxes requesting values for the variables Meta variables can either have the type CML expression or CML action and must correctly parse as such Once all variables and have been entered and accepted the refinement is executed with the variables substituted It should be noted that as a further step to our refinement tool each of the refine ment laws we have implemented should be separately proved as theorems within the Isabelle UTP semantic framework EZW14 within the context of the theory of CML as illustrated in Figure 10 for Maude based refinement This will ensure that our refinements are truly mathematically and foundationally sound Many of our current laws have previously been proved in the context of Circus either by hand or in ProofPower Z Oli06 4 2 Programmatic refinement laws Central to refinement API is the IRefine interface which all refinement law classes must implement A refinement law in general consists of the following 42 D33 4 Refinement Support Public COMPASS elements e a name string get Name e an explanatory detail string getDetail
18. SEVENTH FRAMEWORK PROGRAMME Grant Agreement 287829 Comprehensive Modelling for Advanced Systems of Systems COMPASS Formal Refinement Support Technical Note Number D33 4 Version 1 00 Date September 2014 Public Document http www compass research eu D33 4 Refinement Support Public COMPASS Contributors Simon Foster UY Alvaro Miyazawa UY Editors Simon Foster UY Alvaro Miyazawa UY Reviewers Jan Peleska UB Zoe Andrews Newcastle Lu s D Couto AU D33 4 Refinement Support Public COMPASS Document History Ver Date Author Description 0 01 11 07 2014 Simon Foster Initial document version 0 02 23 07 2014 Alvaro Miyazawa Outline of the report 0 03 15 08 2014 Simon Foster Added initial technical texts 0 04 28 08 2014 SF and AHM Completed MiniMondex and intro duction 1 00 29 09 2014 SF and AHM Responded to comments D33 4 Refinement Support Public COMPASS Contents 1 Introduction 5 2 User Manual 6 3 Case Studies 10 3 1 Chronometer refinement 11 3 2 Distributed mini Mondex 26 4 Technical Overview 41 4 1 Functionality and workflow 41 4 2 Programmatic refinement laws 42 4 3 Maude refinement laws 43 5 Related Work 52 6 Conclusions 52 D33 4 Refinement Support Public COMPASS 1 Introducti
19. Sequential Composition Associativity 2 to the whole action except the hiding in order to group the second specification statement and the parallel action together D33 4 Refinement Support Public COMPASS lt Ea a ans inc minsReq th 12 z K 3 H 5 pre true post min Il o N N D33 4 Refinement Support Public COMPASS ans inc minsReg Next we apply the law Distribute sequential composition over parallelism on the left hand side to the sequential composition of the second specification statement and the parallel action to move the speci fication statement inside the parallel action frame wr min pre true post min 0 sec ans inc minsReg min mu X inc gt frame wr min post min min 1 mod 60 minsReq gt ans min gt Skip ans inc minsReq D33 4 Refinement Support Public COMPASS ans inc minsReg Similarly we apply the law Distribute sequential composition over parallelism on the right hand side to the sequential composition of the remaining specification statement and the parallel action to move the spec ification statement to the right hand side of the parallel action frame wr sec pre true post sec 0 mu X time gt minsReq gt ans mins gt out mins sec gt Skip tick gt frame wr sec post sec
20. a University of Wellington 1993 M V M Oliveira A C Gurgel and C G de Castro CRefine Sup port for the Circus Refinement Calculus In Antonio Cerone and Stefan Gruner editors 6th IEEE International Conferences on Soft ware Engineering and Formal Methods pages 281 290 IEEE Com puter Society Press 2008 IEEE Computer Society Press M V M Oliveira Formal Derivation of State Rich Reactive Pro grams using Circus PhD thesis Department of Computer Science University of York UK 2006 YCST 2006 02 55 D33 4 Refinement Support Public COMPASS OXC04 Vic90 WCO01 WSC 08 ZOC12 M V M Oliveira M Xavier and A L C Cavalcanti Refine and Gabriel Support for Refinement and Tactics In Jorge R Cuellar and Zhiming Liu editors 2nd IEEE International Conference on Software Engineering and Formal Methods pages 310 319 IEEE Computer Society Press September 2004 IEEE Computer Society Press Trevor Vickers An overview of a refinement editor In Fifth Aus tralian Software Engineering Conference 1990 Proceedings The page 39 Institution of Radio and Electronic Engineers Australia 1990 J C P Woodcock and A L C Cavalcanti A Concurrent Language for Refinement In A Butterfield and C Pahl editors IWFM O Sth Trish Workshop in Formal Methods BCS Electronic Workshops in Computing Dublin Ireland July 2001 Jim Woodcock Susan Stepney David Cooper John A Clark and
21. a choice of the three actions above receiving rejecting or executing a request mu X i Index RecTranReg i RejTran i EffTran i X end 29 D33 4 Refinement Support Public COMPASS As a first step of the refinement we simplify the model using the constant values such as N and v process Specl begin state cards seq of Money 10 10 reqs map Index to TransReg gt inv cards 1 cards 2 M and dom reqs subset Else eg N forall mk_ i j in set rng reqs i lt gt j operations AddTranReg Index Index Money gt AddTranReq i j n regs regs il gt mk 1 j n RemReq Index gt RemReq i reqs i lt reqs MkTran Index gt MkTran i atomic cards i cards i reqs i 3 cards reqs i 2 cards reqs i 2 reqs i 3 RemReq i actions RecTranReg i Index i not in set dom reqs amp pay i j 1 lt gt j n n gt 0 gt AddTranReg i j n RejTran i Index i in set dom reqs and reqs i 3 gt cards i reject i gt RemReq i EffTran i Index i in set dom reqs and reqs i 3 lt cards 1 transfer i reqs i 2 reqs i 3 gt MkTran i mu X i Index RecTranReg i RejTran i EffTran i 30 D33 4 Refinement Support Public COMPASS Next we data refine the specification The abstract state is cards seq of M
22. atch State op Unpress gt Button op Coffee gt Button op Tea gt Button op Nothing gt Hatch op CupCoffee gt Hatch op CupTea gt Hatch vars H Hatch vars B Button vars x y Nat op V _ _ _ _ Nat Nat Button Hatch gt State rl V S x 0 Coffee Nothing gt V x S 0 Coffee Nothing rl V S x S 0 Coffee Nothing gt V x S S 0 Coffee Nothing rl V x S S 0 Coffee Nothing gt V x 0 Unpress CupCoffee rl V S x O Tea Nothing gt V x S 0 Tea Nothing rl V x S 0 Tea Nothing gt V x 0 Unpress CupTea 45 D33 4 Refinement Support Public COMPASS endm The module VENDING imports the previous functional module NAT ARITH It declares three sorts to represent the the button hatch and state of the vending machine The button can be in three states unpressed pressed coffee and pressed tea The hatch can contain either nothing a cup of coffee or a cup of tea We declare some variables for use in our rewrite laws Then we create a constructor for the state of the vending which includes a natural number to represent the coins inserted a natural number for the coins accepted the button pressed and the contents of the hatch We then create five rewrite laws to specify the behaviour of the vending ma chine For coffee we have two laws which transfer two coins from inserted to accepted state and for tea one The remaining two l
23. aws dispense coffee or tea once enough money has been inserted We can then used Maude to explore possi ble behaviours We first exemplify the rew command which recursively applies all possible rewrite laws until termination Maude gt rew V S 0 O Tea Nothing Here we ask Maude to fully rewrite the vending machine where we have inserted one coin and requested tea The rew command is also aware of any equations we have specified and will also rewrite the terms appropriately using them After entering this command Maude responds rewrite in VENDING V S 0 0 Tea Nothing rewrites 2 result State V 0 0 Unpress CupTea Two rewrite laws have been applied and the final state is that no coins remain in the system and a cup of tea has been dispensed If we insert an extra coin we get a similar result Maude gt rew V S S 0 0 Tea Nothing rewrite in VENDING V S S 0 0 Tea Nothing rewrites 2 result State V S 0 0 Unpress CupTea However at the end a coin remains in the system In addition to the rewrite com mand Maude includes a lower level search command which can be used to search for applicable laws Maude gt search V S 0 0 Tea Nothing gt 1 V x y B H search in VENDING V S 0 0 Tea Nothing gt 1 V x y B H 46 D33 4 Refinement Support Public COMPASS Solution 1 state 1 states 2 rewrites 1 x gt 0 y gt S 0 B gt Tea H gt Nothing We here requ
24. cardl cardl ml cardl transfer card2 transfer 1 2 x gt card2 card2 x hasl false not has2 pay 2 4 2 lt gt 5 n n gt 0 gt has2 true src2 2 tgt2 j m2 n has2 and m2 gt card2 amp reject 2 gt has2 false has2 and m2 lt card2 and tgt2 1 amp transfer 2 1 m2 gt card2 card2 m2 card2 transfer cardl1 transfer 2 1 x gt cardl cardl x has2 false Next we distribute the guard and sequential composition over the parallelism using the following new laws Law guard par dist g amp c gt A l leol l E gt B 36 D33 4 Refinement Support Public COMPASS g amp c gt A I lcl 1 c gt B Law par seq dist c gt A nsl lf lc ns2 c gt B C c gt A C Insll lcl JIns2l c gt B provided FV B inter FV C The resulting main action is as follows mu X e not hasl pay 1 j 1 lt gt j n n gt 0 gt hasl true srci 1 tgtl j ml n hasl and ml gt cardl amp reject 1 gt hasl false hasl and ml lt cardl and tgtl 2 amp transfer 1 2 m1 gt cardi cardi ml hasl false cardl transfer card2 transfer 1 2 x gt card2 card2 x not has2 amp pay 2 3 2 lt gt j n n gt 0 gt has2 true src2 2 tgt2 j
25. case is just true A slightly more complicated law encoding follows for the guard weakening law rl pre guard weaken refs gl amp A gt rinf guard weaken Guard Weakening gl amp A 92 A provided g2 gt gl meta g2 expression crl guard weaken refine guard weaken lt gl amp A M p gt gt lt getExp M g2 amp A empty gl gt getExp M g2 gt if M g2 undefined and isExp M g2 In this example the precondition states that a single meta variable g2 is required of type expression The actual refinement law is a conditional rewrite law indi cated by crl instead of rl since it relies on this variable being defined and having the correct type The law body uses map lookup written M k to get the value of the meta variable g2 and then extracts the expression within This law also has the proviso that gl g2 and this is also encoded The condition of the law stated after the if states that there must exist a value for g2 in M it cannot be undefined and further that this value must be an expression Of the two kinds of law Maude refinement laws are the easiest to implement once the refinement law DSL encoded above is understood They are not as expressive as programmatic laws the latter being computationally complete and currently cannot make use of other external AST nodes Nevertheless for the majority standard refinement laws the Ma
26. d2 and tgt2 1 amp transfer 2 1 m2 gt card2 card2 m2 has2 false X end process CSpec Cardl transfer Card2 The final process CSpec is a distributed process that refines the original specifi cation Further refinement steps can be applied to rename the state components of the processes Cardi and Card2 and replace them by a parametrised process Card Whilst this development was carried out for a small number of cards the gen eral strategy can be applied for other values of N Furthermore a similar strategy can be applied to refine a version of the model parametrised by the number of cards This development however requires refinement laws that deal with iter ated operators as well as extensions to the language to support partitioning of sequences and mappings in parallel operator Alternatively it may be possible to verify the parametrised model using a strategy based on promotion as discussed in Oh06 We believe that the strategy used to verify this case study provides a general treat ment of SoS contracts and their refinement into a concrete distributed SoS model The overall approach is to first model the contract as a single process encapsu lating a monolithic state over which we can assert global invariants that must be preserved in the SoS This provides an Olympian view of the SoS topology and due to its centralised state supports the use of traditional verification techniques such as simulation
27. e downloaded executable to install Maude to a suitable location Once installed Maude must be setup within Symphony Configure the refine ment tool by selecting menu Windows Preferences Maude Setup as shown in Figure l You must provide the path to the Maude binary or exe file on Win dows and the path to the Maude encoding cml refine maude provided with the tool Symphony will try and detect the location of this file and populate it in advance Next the refinement perspective must be selected as shown in Figure 2 by select ing menu entry Window Open Perspective Other D33 4 Refinement Support Public COMPASS Preferences vv vv vo vv VOY vo vv vo vv vv v General Ant Help Install Update Isabelle Java JavaScript Maude Setup Maven Model Checker Setup Play Plug in Development RT Tester Run Debug Scala Scala Worksheet Symphony Team Theorem Prover Setup Validation VDM Web XML O Maude Setup Sr Setup values for using Maude for refinement Maude binary location usr bin maude Browse Maude CML location home user cml refine maude Browse Restore Defaults Apply Cancel Ok Figure 1 Maude configuration Open Perspective amp Java Browsing 2 fe Java Type Hierarchy amp Javascript mc Model Checker lt gt Plug in Development Bl roc PO Proof Obligation Refinement R Resource Y RttPerspective amp Scala amp Team Synchronizing VDM X XML
28. e used to explore possible rewrites a system can undertake which could for instance specify the behaviour of an abstract machine Due to Maude s powerful search facilities for possible rewrites we considered that it would make an excellent platform for implementing refinement laws inspired by similar work with the rCOS language GLMW 13 We briefly introduce the Maude language with some examples A Maude file con sists of a collection of modules each of which contains a number of definitions There are several types of modules but the two we focus on are called functional 43 D33 4 Refinement Support Public COMPASS modules and system modules The former contain functional specifications in cluding sorts term constructors variables and equations whilst the latter also contains rewrite rules A simple functional module for natural number arithmetic follows fmod NAT ARITH is sort Nat op 0 gt Nat ctor op S Nat gt Nat ctor op Nat Nat gt Nat prec 20 vars x y Nat eq 0 x x eq S x y S x y endfm We declare the module with name NAT ARITH which contains a sort for natural numbers and three operators 0 S and The former two which construct natu ral numbers are declared as constructor operations by use of the ctor directive The third operator an infix plus operator represented a function on two naturals We specify the reduction behaviour for by means of two e
29. en be used to further certify refinements produced by our tool through a process of reconstruction where each law application is substituted for an Isabelle theorem the proven provisos acting as inputs where necessary This then will allow us to fully follow the approach of where Isabelle and Maude work in tandem to provide fully verified and yet highly automated model refinements In terms of our Maude integration the integration is stable but lacking support for a number of things The CML AST representation is only partially complete and in particular there is little support for indexed operations Moreover we currently do not generate and maintain an AST representation of a particular CML file in 53 D33 4 Refinement Support Public COMPASS Maude This is necessary if we wish to make use of contextual information in refinements We will also need some form of edit model for the AST so that the underlying Maude file can be separately maintained Our use of Maude in the re finement tool is currently limited to the use of Maude s unification algorithm and basic search facilities A desirable future feature would be automation of multi ple refinement steps that can be implemented through Maude s powerful search facilities The interface we currently have is quite simple In particular there is currently no management of the refinement state means for instance it is currently impossible to reverse refinement steps properly We a
30. est that Maude give us all possible single step rewrites indicated by the gt 1 into a state matching the pattern V x y B H Maude responds stating that there is one solution and gives values for the variables in our result pattern In this case a single coin has been accepted Alternatively we can request the reflexive transitive closure of the rewrite relation Maude gt search V S S 0 0 Tea Nothing gt x V x y B H search in VENDING V S S 0 0 Tea Nothing gt x V x y B H Solution 1 state 0 states 1 rewrites 0 x gt S S 0 y gt 0 B gt Tea H gt Nothing Solution 2 state 1 states 2 rewrites 1 x gt S 0 y gt S 0 B gt Tea H gt Nothing Solution 3 state 2 states 3 rewrites 2 x gt S 0 y gt 0 B gt Unpress H gt CupTea No more solutions states 3 rewrites 2 47 D33 4 Refinement Support Public COMPASS There are three possibilities each corresponding to one of the states of vending machine operation In the first solution nothing has as yet occurred in the sec ond one coin has been accepted and so on It is this search functionality that we make most use of in our refinement tool for finding applicable laws For more background to Maude please see the manuaf 4 3 2 Refinement in Maude A partial CML AST was implemented in Maude during the COMPASS project by Prof Musab AlTurki from KPUFM in Saudi Arabid
31. f limitations which we leave for future work The refinement provisos can currently not be discharged though a link to the theorem prover plugin exists which should enable this However com plex refinement provisos including further refinements will require a complete theory of CML mechanised in Isabelle UTP which is still a work in progress In a related note the refinement laws implemented in the tool should also be mech anised in Isabelle UTP to ensure that the refinements produced by our tool are correct and well founded The number of laws implemented is also limited and more should be implemented in the future to enable more complex refinements Indeed it is likely necessary that a complete set of laws specifically for SoS refine ment is required to enable a more comprehensive approach to verification against a CML contract The refinement laws we have implemented are adapted from the previous laws for Circus CSW03 which have been separately mechanised in ProofPower Z 0106 However these laws have not as yet been separately validated within the context of our own CML mechanisation based in Isabelle UTP FP13 Since the semantic model of CML does substantially differ from that of Circus this is a necessary step to gain complete confidence in refinements Being a deep embedding Isabelle UTP gives us the basis to precisely specify and prove these laws correct with respect to the underlying theory of CML Once proven these laws could th
32. finement Support Public COMPASS CR88 CSW03 FP13 FZW14 GLMW 13 GNU92 Gru92 Mor90 Nic93 OGdC08 O1106 D A Carrindgton and K A Robinson A prototype program refine ment editor In Australian Software Engineering Conference pages 45 63 ACS 1988 A L C Cavalcanti A C A Sampaio and J C P Woodcock A Re finement Strategy for Circus Formal Aspects of Computing 15 2 3 146 181 2003 Simon Foster and Richard J Payne Theorem proving support de velopers manual Technical report COMPASS Deliverable D33 2b September 2013 S Foster F Zeyda and J Woodcock Isabelle UTP A mechanised theory engineering framework In 5th Intl Symposium on Unifying Theories of Programming 2014 Andreas Griesmayer Zhiming Liu Charles Morisset and Shuling Wang A framework for automated and certified refinement steps Innovations in Systems and Software Engineering 9 1 3 16 2013 Lindsay Groves Raymond Nickson and Mark Utting A tactic driven refinement tool In 5th Refinement Workshop pages 272 297 Springer 1992 Jim Grundy A window inference tool for refinement In CliffB Jones RogerC Shaw and Tim Denvir editors 5th Refinement Work shop Workshops in Computing pages 230 254 Springer London 1992 Carroll Morgan Programming from Specifications Prentice Hall London UK 1990 R Nickson Tool Support for the Refinement Calculus PhD thesis Victori
33. gt seq of nat initseq n V i in set 1 n sum seq of int gt int sum xs if xs then 0 else hd xs sum tl xs measure sumM Two auxiliary functions are declared The first initialises a sequence with the constant V and the second sums the elements of a sequence channels pay transfer Index Index Money The specification uses three channels pay transfer and reject The channel pay is used to request a payment to be made transfer is used to complete a payment request and reject is used to indicate that the payment cannot be completed The process that specifies the system declares two state components cards and req The first is a sequence of Money and stores the balance of each card of type Index and the second is a mapping of TransReg that records the transference requests that have not yet been completed or rejected The state invariant is spec ified that requires the sum of the balances of all cards to be equal to M that the originator of a transfer request to be one of the cards and that it is not possible for a card to transfer money to itself process Spec begin state cards seq of Money initseg N reqs map Index to TransReq gt inv sum cards M and dom reqs subset inds cards and forall mk i 5 in set rng reqs i lt gt j Three auxiliary operations are declared to simplify the manipulation of the state AddTrankReq adds a transference request to the
34. he assumption falsifies the guard it is possible to remove that branch of the external choice mu X e not hasl pay 1 3 1 lt gt j n n gt 0 gt hasl true srci 1 tgtl j ml n hasl and ml gt cardl amp reject 1 gt hasl false hasl and ml lt cardl and tgtl 2 transfer 1 2 m1 gt cardl cardl ml card2 card2 ml hasl false not has2 amp pay 2 j 2 lt gt j n n gt 0 gt has2 true src2 2 tgt2 j m2 n has2 and m2 gt card2 reject 2 gt has2 false has2 and m2 lt card2 and tgt2 1 amp transfer 2 1 m2 gt card2 card2 m2 cardl cardl m2 has2 false X In the next step we parallelise the assignment to card1 and card2 of the two choices prefixed by transfer 35 D33 4 Refinement Support Public COMPASS Law seq par intro c gt vl el v2 e2 c gt vl el livl l lcl l v2 c gt v2 e2 provided vl lt gt v2 vl not in set usedV e2 and v2 not in set usedV el The novel refinement law above is used twice to complete this step mu X not hasl amp pay 1 3 1 lt gt j n n gt 0 gt hasl true srci 1 tgtl j ml n hasl and ml gt cardl amp reject 1 gt hasl false hasl and ml lt cardl and tgtl 2 amp transfer 1 2 mi gt
35. ialises the state and starts a loop mu X F X that at each step calls the action Run process AChronometer begin state sec RANGE min RANGE actions AInit frame wr sec min pre true post sec 0 and min 0 12 D33 4 Refinement Support Public COMPASS incSec frame wr sec pre true post sec sec 1 mod 60 incMin frame wr min pre true post min min 1 mod 60 Run tick gt incSec sec 0 amp incMin sec lt gt 0 amp Skip time gt out min sec gt Skip AInit mu X Run X end We wish to verify that this process is refined by a concrete process that controls the storage of seconds and minutes in parallel components This concrete spec ification uses three extra channels inc minsReq and ans The first is used to request that the minutes are incremented the second is used to request the current value of the state component minutes and the third is used to obtain the answer to the request of minsReq channels inc minsReq channels ans RANGE The parallel process declares the same state as the abstract process and six ac tions SecInit initialises the component sec MinInit initialises min incSec increments sec incMin increments min RunSec accepts requests to increment the time or output the elapsed time and RunMin accepts request to increment the minutes or output the elapsed minutes The main action of this process is the parallel
36. ially programmatically 3 display applicable laws in a list for the user to select 4 when a user selects a law request any meta variables required to complete the refinement step 5 apply selected law to the AST fragment updating the CML document tree and adding any necessary provisos to the list of refinement proof obliga tions This step is performed via a text edit to the CML file Refinement provisos usually take the form of propositional formulae which must be discharged by a theorem prover for the refinement to be correct Consider the following law for example pre p post q Skip provided p gt q Here the refinement proviso is p gt q which should be discharged by the CML theorem prover FP13 If it cannot be discharged the refinement is unsubstanti ated and future refinements are therefore invalid Nevertheless refinement with out discharge can be useful for experimental and speculative refinement where a particular result is desired Currently discharge of provisos is unsupported by the tool though a link to the theorem prover exists in Symphony and we propose to 4 D33 4 Refinement Support Public COMPASS Symphony LA Execute Refinement Refinements Provisos a 4 Maude Figure 10 Overview of the interaction in the refinement tool enable its integration in the future Moreover the potential exists for using other components of Symphony to discharge provisos such as the CO
37. ification using the refinement calculus An overview of this re finement is shown in Figure 8 The abstract specification declares a type RANGE of natural numbers between O and 59 that is used to encode minutes and seconds types RANGE nat inv i i lt 60 It also declares three channels tick time and out The first marks the passage 11 D33 4 Refinement Support Public COMPASS Abstract Process Concrete Process 1 1 a 1 1 1 1 out i A inc minsReq tick time Figure 8 Refinement of the Chronometer of 1 second the second requests the current time and the third answers to the request with the number of minutes and seconds that have elapsed channels tick time out RANGEX RANGE The process that models the abstract chronometer is called AChronometer and declares a state formed by two components sec and min The processes declares four actions AInit incSec incMin and Run AInit initialises the state com ponents incSec increments sec and incMin increments min The action Run offers a choice of synchronising on tick or time In the first case the seconds are incremented using incSec and if the result is zero the minutes are incre mented otherwise the action terminates In the second case synchronisation on time the values stored in the state components are communicated through the channel out The behaviour of the process AChronometer is given the main action after which init
38. inement The Mini Mondex case study models a card system where the main desirable properties are that 1 money is not created or lost during the operation of the system and 2 that the implementation of the system be based on fully distributed cards where each card records its available balance Whilst it is feasible to specify property 1 in a centralised specification as an in variant of the state it is not possible to do so in a distributed specification in which the amount of money available to each card is only visible to the card itself Our approach to obtain a distributed system that preserves property 1 is to start from a centralised specification that enforces this property and refine it into the distributed version whilst preserving the invariants as shown in Figure p The centralised specification is shown below values N nat 2 V nat 10 M nat NxV It declares the number N of cards the initial balance of each card v the total amount of money in the system M types Index nat inv i i in set 1 N Money nat inv m m in set 0 M TransReq Index Index Money 21 D33 4 Refinement Support Public COMPASS Next three types are declared Index encodes the indices of the cards Money the possible balance values and TransReq encodes a transference request formed by the index of the payer the index of the payee and the amount of money being transferred functions initseq nat
39. lso need to be able to save the refinement state so that it can be continued and rolled back later if necessary Also we do not currently have integration with other tools for example the theorem prover and the model checker the latter of which would be used to discharge certain kinds of action refinements References BHS92 R J R Back J Hekanaho and K Sere Centipede a program re finement environment 1992 BW90 R J R Back and J Wright Refinement concepts formalised in higher order logic Formal Aspects of Computing 2 1 247 272 1990 BW98 Ralph Johan Back and Joakim Wright Refinement Calculus A Sys tematic Introduction Springer 1998 CDE 99 M Clavel F Durn S Eker P Lincoln N Marti Oliet J Meseguer and J F Quesada The maude system In Rewriting Techniques and Applications Springer LNCS1631 1999 CDE 07 Manuel Clavel Francisco Dur n Steven Eker Patrick Lincoln Nar ciso Marti Oliet Jos Meseguer and Carolyn L Talcott editors All About Maude A High Performance Logical Framework How to Specify Program and Verify Systems in Rewriting Logic volume 4350 of Lecture Notes of Computer Science Springer Verlag 2007 CHN 94 David Carrington lan Hayes Ray Nickson Geoffrey Watson and Jim Welsh A review of existing refinement tools Technical Report 94 8 Software Verification Research Centre Department of Com puter Science The University of Queensland 1994 54 D33 4 Re
40. m2 n has2 and m2 gt card2 amp reject 2 gt has2 false has2 and m2 lt card2 and tgt2 1 transfer 2 1 m2 gt card2 card2 m2 has2 false card2 transfer cardl transfer 2 1 x gt cardl cardl x xX Next we apply the following novel law to transform a recursion of external choices into a parallelism of recursions Law rec ext par rec 37 D33 4 Refinement Support Public COMPASS mu X al gt Al a2 gt A2 b gt B wrtV B1 lbl wrtV B2 b gt B2 ci gt CE ez gt C2 X mu X al gt Al cl gt C1 b gt Bl X wrtV A1 B1 C1 b wrtV A1 B1 C1 mu X a2 gt A2 c2 gt C2 b gt B2 X provided FV Al union FV B1 union FV C1 inter FV A2 union FV B2 union FV B2 The result action is as follows e mu X not hasl amp pay 1 3 1 lt gt j n n gt 0 gt hasl true srci 1 tgtl j ml n hasl and ml gt cardl reject 1 gt hasl false hasl and ml lt cardl and tgtl 2 amp transfer 1 2 m1 gt cardi cardi ml hasl false transfer 2 1 x gt cardl cardl x X cardl has1 src1 tgt1 ml transfer card2 has2 src2 tgt2 m2 1 mu X transfer 1 2 x gt card2 card2 x not has2 am
41. map reqs RemReq removes a 28 D33 4 Refinement Support Public COMPASS request from reqs and MkTran executes a transference request by withdrawing money from the payer s card and adding it to the payees card operations AddTranReg Index Index Money gt AddTranReg i j n regs regs il gt mk 1 j n pre i lt gt 5 RemReq Index gt RemReq i reqs i lt reqs MkTran Index gt MkTran i atomic cards i cards i reqs i 3 cards reqs 1 2 cards reqs i 2 reqs i 3 RemReq i Next three auxiliary actions are declared each specifying the possible interac tions with the system The first RecTranRea offers the possibility of requesting a payment through the channel pay from a card i RejTran rejects any requests from card i that cannot be completed due to insufficient funds and EffTran executes any requests from card i that can be completed actions RecTranReg i Index i not in set dom reqs amp pay i j i lt gt 3 n n gt 0 gt AddTranReq i j n RejTran i Index i in set dom reqs and reqs i 3 gt cards i reject i gt RemReq i EffTran i Index i in set dom regs and reqs i 3 lt cards 1 transfer i reqs i 2 reqs i 3 gt MkTran i Finally the overall behaviour of the process is specified by a recursive action that at each step offers for each of the cards
42. nement Support Public COMPASS src2 Index tgt2 Index m2 Money inv cardl card2 20 and hasl gt srcl in set 1 2 and has2 gt src2 in set 1 2 and hasl gt srci lt gt tot1 and operations AddTranReq Index Index Money gt AddTranReq i j n cases i 1 gt hasl true srci i tgtl 2 gt has2 true src2 i tgt2 end RemReq Index gt RemReq i cases i 1 gt hasl false 2 gt has2 false end MkTran Index gt MkTran i cases i 1 gt cardl cardi ml cases tgtl 1 gt cardl cardl ml 2 gt card2 card ml end RemReg 1 2 gt card2 card2 m2 cases tgt2 1 gt cardl cardl m2 2 gt card2 card2 m2 end RemReq 2 end actions RecTranReg 1 1 Index 1 gt not hasl and i 2 pay i j i lt gt j n n gt 0 RejTran 1 Index 32 j j gt not has2 gt AddTranReq i has2 gt src2 lt gt tgt2 ml n m2 n amp j n D33 4 Refinement Support Public COMPASS i 1 and hasl or i 2 and has2 and 1 1 and ml gt cardl or i 2 and m2 gt card2 amp reject i gt RemReg i EffTran i Index i 1 and hasl or i 2 and has2 and 1 1 and ml lt cardl or i 2 and m2 lt card2 1 1 amp transfer 1 tgt1l ml gt MkTran 1
43. of the beginning and end of the selection Next the applicable laws can be searched by right clicking on the excerpt and selecting Refinement Refine or pressing Ctrl 6 as shown in Figure 5 D33 4 Refinement Support Public COMPASS aiii a e G 4 Q E EJcML c Refinement E cmL Explorer 23 E test cml 8 O C Refinement Laws jm e amp channels c nat Law Name j v test process test begin Eltest cml tare a v nat 1 actions B val x nat Stop A Biv end E CMLRPOList 23 ul Ne Re Type Source E Refinement Law Details 2 o lt Refinement Laws gt E CML RPO Details 53 ml writable Insert 8 26 me fis dE la rr ve a E Bom c Refinement EJ cML Explorer 5 z B test cml 5 E E Refinement Laws E fm a S channels c nat Law Name Y test process test begin Eltest cml stete a v nat 1 actions R B val x nat Stof B v Open With pi Show In Shift Alt w Cut Ctrl x E CMLRPOList 5 Sl 1 copy atire Ne Re Type Source Paste Ctrl v Quick Fix Ctrl 1 shift Right Shift Left E Refinement Law Details 33 a RC openDecleration r3 L lt Refinement Laws gt Debug As Ip Run As E CML RPO Details 3 ow CI Validate o E Team Compare With Replace With Fault Tolerance Refinement Refine Ctrl 6 Preferences Input Methods Insert 8 26 Figure 5 Searching for applicable laws D33
44. on This deliverable describes the implementation of the CML formal refinement tool Refinement is a verification and formal development technique pioneered by Ralph Johan Back BW98 and Carroll Morgan Mor90 It is based on a behaviour preserving relation that allows the transformation of an abstract specification into more and more concrete models potentially leading to an implementation One of the key aspects of refinement is the reduction of non determinism which is a common abstraction mechanism used in specification languages CML provides various abstraction mechanisms including implicit operations spec ification statements non deterministic choice etc Its refinement calculus which is derived from the Circus refinement calculus Oli06 supports both action refinement as in CSP and data refinement as in Z and VDM and pro vides a framework for the development and verification of distributed state rich specifications The COMPASS refinement tool enables a user to apply refinement laws to a CML model thus transforming it to a new model retaining existing behaviour whilst reducing non determinism This enables a developer to 1 refine a concrete con stituent system from an abstract specification and 2 demonstrate that a given sys tem satisfies or does not satisfy a suitable Systems of Systems SoS contract The latter is explored in more detail in Section 3 2 The tool ships with an initial set of refinement laws including
45. oney reqs map Index to TransReq The concrete state encodes the sequence of size 2 of the abstract models as two state components cardi and card2 and the map as eight state components that identify whether there is a transaction request associated with the card N hasN who is the source srcN who is the target t gtN and how much money is to be transferred mN It is shown below cardl Money card2 Money hasl bool srci Index tgtl Index ml Money has2 bool src2 Index tgt2 Index m2 Money The retrieve relation formalises the relationship between abstract and concrete states and is as follows reqs 1 gt mk_ 1 y z y lt Index z lt Money hasl and y tgtl and z ml munion 2 gt mk_ 2 y z y lt Index z lt Money has2 and y tgt2 and z m2 cards cardl card2 The retrieve relation specifies that a request from card 1 is in the map reqs if and only if the concrete component has1 and in this case the second component of the request is equal to tgt 1 and the third component equals m1 The case for requests from card 2 is similarly specified The sequence of cards is simply the concatenation of the concrete components card1 and card2 The result of data refining the process is shown below process Spec2 begin state cardl Money 10 card2 Money 10 hasl bool false srcl Index tgtl Index ml Money has2 bool false 31 D33 4 Refi
46. p pay 2 j 2 lt gt j n n gt 0 gt has2 true src2 2 tgt2 j m2 n 38 D33 4 Refinement Support Public COMPASS amp reject 2 gt has2 false 1 m2 gt card2 card2 m2 has2 and m2 gt card2 has2 and m2 lt card2 and tgt2 1 amp transfer 2 has2 false X Finally we apply a process refinement law to split the process into the parallel composition of two other processes Card1 and Card2 process Cardl begin state cardl Money hasl bool srcl Index tgtl Index ml Money mu X hasl and ml hasl and ml transfer 1 not hasl pay 1 j hasl true gt cardl amp reject lt cardl and tgtl 2 m1 gt cardi 10 false srel 1 tgtl hasl fal transfer 2 X end process Card2 se 1 x gt cardi fal begin state card2 Money has2 bool src2 Index tgt2 Index m2 Money se 39 1 lt gt j n n gt 0 gt j ml n 1 gt hasl false 2 amp cardl ml cardl x D33 4 Refinement Support Public COMPASS mu X Q transfer 1 2 x gt card2 card2 x not has2 pay 2 4 2 lt gt 5 n n gt 0 gt has2 true src2 2 tgt2 9 m2 n has2 and m2 gt card2 amp reject 2 gt has2 false has2 and m2 lt car
47. quations which use two variables x and y which we declare to have type Nat The standard defini tion for natural number addition then follows We can then use Maude to perform reductions using our equational laws using the red command Maude gt red S S 0 S 0 and Maude responds thus reduce in NAT ARITH S S 0 S 0 rewrites 3 result Nat S S S 0 Three applications of the equational laws show that 2 1 3 System modules are similar to functional modules but in addition can also specify rewrite laws For example mod CLIMATE is sort weathercondition Op sunnyday gt weathercondition op rainyday gt weathercondition rl raincloud sunnyday gt rainyday endm 44 D33 4 Refinement Support Public COMPASS This simple specification declares a sort weathercondition and two pos sible states sunnyday and rainyday We then declare a rewrite law with the name raincloud which transforms a sunnyday toa rainyday Maude can then be used to apply this law which it does by pattern matching against the left hand side and then rewriting Rewrite laws in Maude can also be conditional depending on a true valuation for a given Boolean formula written over the vari ables in the rule left hand side A more complex example follows representing a simple vending machine The vending machine produces tea for one coin and coffee for two coins mod VENDING is pr NAT ARITH sorts Button H
48. s Morgan s refinement calculus CRefine supports refinement of Circus specifications They only support partial verification of proof obligations and do not seem to have support for user defined refinement laws Finally the Circus language and the refinement tactic language ArcAngel have been mechanised in the theorem prover ProofPower Z thus providing support for mechanised refinement While new rules can be added and the tools support discharging proof obligations there is currently no specific user interface for do ing this 6 Conclusions We have presented our implementation of the refinement tool for CML This tool allows an abstract model to be transformed into a concrete possibly executable 52 D33 4 Refinement Support Public COMPASS model through application of a collection of refinement laws We have imple mented an interface for searching for and then applying suitable laws to nodes of the CML AST Refinement laws can be specified either programmatically in Java or else using a simple DSL we have implemented in the Maude rewrite system We have also applied this tool to a simple example and believe in the future this tool could be applied both to refinement of constituent system models Moreover through implementation of further refinement laws for CML it can also be ap plied to proving how a System of Systems satisfies its contract as demonstrated in Section Nevertheless the tool currently faces a number o
49. some of those described in and other sources This initial set is extensible either by implementing them programmatically or by specification in Maude rewrite logic engine CDE 99 CDE 07 It is worth mentioning that while the refinement tool does not attempt to prove the refinement laws the link between the refinement tool and the theorem prover can record the dependency between the soundness of the refinement and the soundness of the laws though the latter is out of the scope of this deliverable This deliverable is structured as follows Section 2 describes how to install and use the tool Section 3 describes two verification case studies developed in the context of task T3 3 4 a simple chronometer and a more complicated example based on a simplified version of the Mondex electronic purse WSCtO8 The latter case study also provides an insight into the verification of emergent properties in an SoS Section 4 describes the implementation of the tool as well as the steps necessary to extend the catalogue of refinement laws Finally Section 5 describes related tools and Section 6 summarises our results and discusses limitations and future work D33 4 Refinement Support Public COMPASS 2 User Manual This section describes the use of the refinement tool plug in which is distributed with the Symphony IDE versions 0 3 6 This plug in takes CML specifi cations and supports the application of refinement laws This plug in c
50. to the auxiliary actions and further simplify the specification obtaining the following main action mu X not hasl pay 1 3 1 lt gt j n n gt 0 gt hasl true srci 1 tgtl j ml n hasl and ml gt cardl reject 1 gt hasl false hasl and ml lt cardl amp transfer 1 tgtl ml gt cardl cardl ml tgtl 1 amp cardi cardl ml hasl false tgtl 2 card2 card2 ml hasl false 34 D33 4 Refinement Support Public COMPASS not has2 amp pay 2 3 2 lt gt j n n gt 0 gt has2 true src2 2 tgt2 j m2 n has2 and m2 gt card2 amp reject 2 gt has2 false has2 and m2 lt card2 amp transfer 2 tgt2 m2 gt card2 card2 m2 tgt2 1 amp cardl tgt2 2 card2 card2 m2 has2 cardl m2 has2 false false Next we use the invariant that forbids self requests to remove the choices guarded by tgt1 1 and tgt2 2 This is necessary because the expansion of the operations includes options that do not occur under certain circumstances but cannot be eliminated without explicit reference to the invariant In order to elimi nate the unreachable operations we introduce the invariant as an assumption and distribute it through the action until it reaches the guards introduced by the ex pansion of the operations If t
51. uction mu X tick gt frame wr sec post sec sec 1 mod 60 sec 0 amp frame wr min post min min 1 mod 60 sec lt gt 0 amp Skip time gt out min sec gt Skip X The law Specification Sequential Introduction is applied to the first specification statement and breaks it into two statements in sequential com position Next we refine the recursion mu x into a parallelism of recursions using the law Parallel Recursion Distribution with Hiding with pa rameters ns2 min cs inc minsReg ans nsl sec 17 D33 4 Refinement Support Public COMPASS A2 RunMin Al RunSecand Sync inc minsReg ans This law is a specialisation of the fixed point law in and as such generates a pro viso of the form A B which can be verified through model checking theorem proving or the refinement tool via a separate refinement frame wr min pre true post min 0 frame wr sec pre true post sec 01 frame wr min pre true post min 0 frame wr sec pre true post sec 01 mu x ESSE x sec ans inc minsReq min mu x EM x AN ans inc minsReg Again we apply the law Copy Rule from Left to Right to remove the calls to RunSec RunMin o frame wr min pre true post min frame wr sec pre true post sec mu X Il o sec
52. ude approach is best Thus far we have only implemented a small number of laws 20 but along with the programmatic refinement laws this is sufficient to support the example in Section 3 1 51 D33 4 Refinement Support Public COMPASS 5 Related Work Various tools have been previously developed to support formal refinement The following descriptions are based on CHN 94 and ZOC12 RED Vic90 is a refinement tool that supports the application of Morgan s refine ment calculus but does not support the verification of proof obligations RED is no longer available The tool described in Nic93 and GNU92 supports Morgan s refinement calcu lus and provides some support for discharging proof obligations This tool is also no longer available Centipede BHS92 supports the refinement of specifications and guarded com mands extended with features of action systems Verification of proof obliga tions is delegated to the theorem prover HOL This tool is also no longer avail able The tool described in CR88 supports only a limited procedural language and is also no longer available A number of HOL based refinement tools have been developed by BW90 and Gru92 BW90 supports Back s refinement calculus Neither of these tools seem to be available To the best of our knowledge the only refinement tools for calculation currently available are Refine and the related tool CRefine OGdC08 While Refine support
53. urrently contains a number of simple laws but can be extended with new refinement laws in two different ways implementing the refinement law in Java or encoding the refinement law in Maude In general the latter option is simpler more powerful less error prone and does not require recompilation of the plugin However for certain types of laws for instance the copy rule that replaces an action call by its definition it is easier to implement directly in Java due to the need to search the specification for the definition of the action being called Details of how the refinement tool can be extended with new laws is given in Section 4 It is important to notice that the use of Maude refinement laws is optional In order to use Maude in the refinement tool it is necessary to first install Maude Maude is available for the three main platforms Linux OS X and Windows at time of writing the latest version is 2 6 For Linux and Mac please visit the Maude website at http maude cs uiuc edu download download the binary archive and then extract the archive to a suitable location Alternatively Maude is available in the apt repos itories for both Debian and Ubuntu and can be installed easily with apt get install maude For Windows please visit the MOMENT project website athttp moment dsic upv es select the Downloads menu and click on Maude for Windows from which you can download the archive for Maude 2 6 on Windows Run th
54. x example is slightly more com plex and aims at demonstrating the suitability of the refinement calculus for the verification of emergent properties of distributed systems Due to its complexity this example cannot be developed using Symphony however suitable extensions 10 D33 4 Refinement Support Public COMPASS Br E amp 4 Sl Qrar ve wer Q E Bom E Refinement EJ cm Explorer X O Ed test cml 2 E C Refinement Laws X El alg gt channels c nat Law Name Y test process test begin gt EJ test cml state B v nat 1 actions A mu XX true amp c v gt XX B val x nat Stop A B v end E CML RPO List 2 10 Ne Re Type Source E Refinement Law Details 5 arg N A N mu X A X E CMLRPO Details E o writable Insert 13 4 Figure 7 Application of refinement law data refinement and new refinement laws of the refinement plugin suffice to sup port this example All the refinement laws used in these case studies unless otherwise states have been previously published in Oli06 Novel laws are presented in the body of the text 3 1 Chronometer refinement In this section we present the example of a chronometer that is implemented through parallel processes This example was first introduced in Oli06 it spec ifies a centralised abstract chronometer AChronometer and a parallel concrete implementation Chronometer and proves that Chonometer is a refinement of the abstract spec
Download Pdf Manuals
Related Search