A Modal Interface Compositional Analysis Library User's guide
Contents
1. 12 55 walk project Signature gt nterfesce gt interface Several modal patterns can be used to help the definition of modal interfaces C PQPbUerms s lever nas EUR rouen Tea Wiehe a enter een such that for every occurrence of word u the last event ONE Wi Ines iwoceliny Wise ECS STE mei D Ge raa e lal ahs not in signature g ot oc ot o FF X val every muore o o CAES EET E gt nee hee lever sense eue ue SON LE Cote Creuse g such that after every occurrence of word u last event excepted the Last event Of ul Mas modality cannot Exception MIGNON CURE is Teens L mene Wi tee ine Mie ETS RE UE e o ot F X ucc cu Me nne qeu gt RET E MINCE C areor imusta Ss Cl OT o ue ein MarcmmeicS wit RCE EDU TES such that after the occurrence of a word accepted by expression x event e has modality must Exec exo WES wemesel mim lt CON e user OEM Tuo Signature g oot o ob ot FF oo F puc INN ecc NME XOM SSTIONL gt Wwe E uu e euge creme stor ene op brod e euge Ses ede o Edo prre nore OM such that after the occurrence of a word accepted by expression x event e has modality cannot KOS ETO Error AMEN EE RS CINE lt ore Si ses mow E signature g o ot o F valfarter annot egnar CE Mores en A ue Ii NIC Maximal consistent subsets of a set of interface can be computed with the following function Imak eO S Te tent SOUS se cCo2. value run val tr Inter value lt abstr gt val ti Inter values lt abstr gt val td Inter value lt abstr gt val tg Inter value lt abstr gt valgo i Inter value lt abstr val qo Inter value lt abstr gt 14 Define a signature consisting of two input events let sigma entry gate receptive new cignature n aput Avs trues input vo false derine as o tere neas Ca Define an interface on the signature defined above let itf entry gate receptive ey Me ihece Sicite Cwiiey Cee T serie state CIS mast ge D vs false g 1 must g 0 Are Erue g 2 May g vs Tae a 1 Mist ee Kh v3 truc q T muot Gace 7s false g 1 may Gg 2 v gt true g 2 derine eer race in Display the interface i CS Oley Charsrece Wier eec ES a a vehicule sense false Define and display two other signatures and interfaces vehicule sense true let sigma entry gate request new sc cite input vs true input vs false JEDE ti deminer cue DE eu let itf entry gate request NeW TIEF CE SO eie Celtics TEH apu eC MB CR CN EO ee ODE may G 0O ys false o 1 may q 0 vs true g 2 may g t vs false g 1 mas ge vs eq ings cp lS se May G 2 vs false g 1 may 2 vs true g 2 MUS ccc E may g 3 v9 false Gg 1 may g o v2 true 2 na eer NEIGE CURE Jerine TEES TC Ce vehicule
3. E ba P d vehicule sense true E 2x ipai duda i 3 ticket request vehicule sense false vehicule sense false vehicule sense false vehicule sense false veh 1 vehicule sense true ticket request vehicule sense true ticket discard cate close ense false vehicule sense true ORGANES vehicule_sense true ticket_request ria 3 V hicule sense false ate open a cket_request ticket_grasp vehicule sense false ticket_request ticket_request vehicule sense true vehicule sense true PLE t vehicule_sense true ticket_request ense false cm ticket_grasp vehicule_sense falsq chicule_sense false L B aa y Pd k 1 1 4 vehicule sense true SE f vehicule sense false vehicule sense true 17
4. compulsory A E LT S S S Two structural composition operators are available in Mica The product operator reflects the parallel composition of systems at the level of interfaces The optimistic parallel composition takes care of input output incompatibilities In essence it computes the least assumption under which every event sent by one component can be received by the other Mica also implements two residuation operators The quotient operator 1s the adjoint of the product S S S2 iff S S lt S5 and the weak implication is a weak adjoint of the conjunction meaning that S lt S S implies S S2 lt S However the converse implication does not hold in general Interfaces can be compared with the refinement preorder relation Several generic properties can be checked on interfaces consistency completeness and triviality Downloading compiling and installing Mica This software can be download at http www irisa fr s4 download mica The distribution contains several folders src source code doc documentation and examples simple use cases It compiles runs and has been tested on the following platforms e Linux e MacOS X version 10 4 or later It should compile and run on the following platforms However this has not been tested e Solaris OpenBSD FreeBSD e Windows NT 2000 XP Vista 7 with Cygwin This software requires the following tools The GraphViz graph mappi
5. source distribution under the CeCILL C Free Software License Agreement version 1 Users agree to comply with the terms of the license contained in the following document http www cecill info licences Licence_CeCILL C_V1 en html Modal interfaces Modal interfaces are automata theoretic specifications with input and output events that can be used capture imprecise or incomplete requirements on the behavior of a system under design They are deterministic transition systems with two kinds of transitions must and may Must transitions are mandatory meaning that every correct implementation of the specification 1s compelled to realize them while may transitions are optional For instance systems M and M are correct implementations of modal interface S given below In these figures states in the shape of a diamond are initial On the contrary system M 19 not an implementation of S The reason is that after performing event b the system refuses to perform event c while in the interface this event has modality must Remark that M is more involved than M since the decision to realize a may transition or not is history dependent Modal interfaces can be combined in many different ways thanks to the conjunction product and quotient operators For instance the figure below details the conjunction of S and S where S is an interface expressing the property that after an even number of occurrences of event b event a is
6. value gt expression gt expression val concat expression gt expression gt expression val sum expression gt expression gt expression val star expression gt expression val shall value gt expression val shallnot value gt expression Generates an interface from an expression valine cR ceo EU MICE Mimi dec The following functions can be used to print values signatures systems and interfaces printers for the above types valgprint c SURESNES NA Udi MANETTES One CENSURE unie welll joc Tate e eva enke SISSE Su UNE Naik iets Wine Sedi E CON Nie uc EOD EE PCS HONEC peccans ul aie Statistics about the heap or a given interface are printed by the following functions Sn Stee SE CCM 1 CN MES SIC ARE OS E oe Me le TT Welk SLR S CES ones ME TT e Wile Print informations about Interfaco and systems val info LIMES te eer bre tr Ce UnLE Systems and interfaces can be drawn with the following functions The graphs can be saved as dot GraphViz files It 1s also possible to retrieve in the tmp directory a svg or pdf file depending on the platform operating system Display systems and interfaces wei Gusto sis T MEN SET gt SCC ON Ci LC ER EN Wile Neill R play Inter ace Linea mmc menie qe nue Generates dot files from systems and interfaces Neill He emo ESS SNS TOME Svs OT L cce ocu rer EL Mum file nane UMS Nell Clone rle MEE CE ingertace gt stri
7. Mica A Modal Interface Compositional Analysis Library User s guide Benoit Caillaud benoit caillaud inria fr INRIA Rennes Bretagne Atlantique Campus de Beaulieu 35042 Rennes cedex France version 0 08a April 10 2014 Introduction Mica is an Ocaml library implementing the Modal Interface algebra published in the following paper Jean Baptiste Raclet Eric Badouel Albert Benveniste Benoit Caillaud Axel Legay Roberto Passerone A Modal Interface Theory for Component based Design Fundam Inform 108 1 2 119 149 2011 The purpose of Modal Interfaces is to provide a formal support to contract based design methods in the field of system engineering Modal Interfaces enable compositional reasoning methods on I O reactive systems In Mica systems and interfaces are represented by extension However a careful design of the state and event heap enables the definition composition and analysis of reasonably large systems and interfaces 10 states The heap stores states and events in a hash table and ensures structural equality there is no duplication Therefore complex data structures for states and events induce a very low overhead as checking equality is done in constant time Thanks to the Inter module and the mica interactive environment users can define complex systems and interfaces using Ocaml syntax It is even possible to define parameterized components as Ocaml functions Mica is available as an open
8. e type signature system and interface I O signatures type signature itype system wo component rad mcn c Poms im Poems TEST Ee MATE AGe e aee e Comocmene loonaeyLotal wee 53 type interface type expression modal regular expressions on events type expression Values and regular expressions are allocated in a heap A hash table allows to retrieve values very quickly and the heap is organized so that every value or regular expression has a unique representation Thanks to this data structure equality can be checked in constant time a very important feature when computing on large state spaces The following function can be used to initialize or reset the heap new Session UNI PT UNS the nheap yal Inc E 2 Unit gt Unit Values can be identifiers characters strings booleans integers and tuples and sets of values The following functions can be used to construct values in the heap Value factory 7 val rident lt String value well e a A ONES so a e val ern NS LOS I vali ET Dool EET waline eu nec vale val tuple value array value Val set value list gt value Regular expressions are used to define modal patterns a library of generic modal interfaces The following functions can be used to define regular expressions and turn them into modal interfaces Regular expression factory val empty unit gt expression val epsilon unit gt expression val prefix
9. es can be made minimal with the following function It implements an algorithm based on the computation of the largest congruence of the interface Comas dme ziem Si minimizes invertace ISIN val Minimize rnterftace gt rnterrace The structure of states becomes more and more complex when iterating on composition operators Although this 1s not really an 1ssue regarding computational complexity this can obfuscate the graphical display of a modal interface The following function simplifies the state structure of a modal interface by computing an injective mapping from the set of reachable states to integers simolity s Simplifies the state structure of interface Isl by mapping state labels to integers Val simplify interface gt interface Whenever an interface needs to be inspected and its state structure is too complex to be represented graphically projections on a sub alphabet turns out to be helpful The projection of C on sub alphabet L is the least abstraction of C with signature L s lalbstract loa computes a projection of interi ce al on sub alpmhabet 12 The resulting interface is the least abstraction of a in the class of interfaces over alphabet 1 2 rel ebot iaee welue List gt TEST gt Ire Ci E L project s al COMPUTES a projection Of interface lal om Signature SI Ihe resulting interface is the largest projection of a that is permissive to Samus nes Controlo nire UE Ss
10. interface block also defines the inconsistent interface void forces the current interface to be inconsistent Wale void T c SUN Function init can be used to define the initial state s of systems and interfaces Systems should have at least one initial states Interfaces can have zero or one initial state init gq defines value gq as initial state of the current system or interface val imit s yvalue gt unit The transition relation of a system is defined by enumerating its transitions Each transition is defined by defined with the trans function erans g e gl detines a transition lal le Sa im the currents system Wiel elections well IE ET vee eae For interfaces modal transitions are defined with the four following functions Cannot 1s the default modality may g se CC aec Runescape ans Lionel la um val may value gt value gt value gt unit AS must g e na i deftiness a may tCranoition Tgi lei ka ijn val must value gt value gt value gt unit inconsistent q e sets event e to be inconsistent in state q ValeinecoOnelorenu value wells UE cannot g el sets event g to cannot in state a S aano E e MUR adus E System s and Interface s signatures can be retrieved with the following functions PEACE UE De omo HE returno thes rogna ture Tir vaste Sun li e Ma onae ureno a en aa CET are oona tur Sor nee re ler eurn Velie mom cou Neer D vale
11. mouTres wine dq ei CINE TIM GOs TESTE TQUE SUIS Sins ue x elie tal rs an array Of pairs Tdenvitier interia e 13 i Wek Wiss COomeLsineme Ses s e e CC cic cc ep ise r Example Examples can be found in folder examples Follow instructions in file readme txt located there The parking use case is detailed below Shell and Mica command line input is colored blue while tool output 1s colored yellow Start the Mica interactive environment Objective Caml version 3012 1 K A ACkCckck Ko kCck ck Kok Ck ck Ko CK KK S MK KM SK GM UK GS KK XM KG KG KK XM KG KG KK KG KG KG KK KO M Kk KK KO MAG K KK MK MA KC Kk ko Kok ck EX EX K K Mica A Modal Interface Compositional Analysis Library Benoit Caillaud INRIA Rennes lt Benoit Caillaud inftia fr Informatique et Automatique September 2011 Distributed under the CeCILL C Free Software Licence Agreement Copyright Benoit Caillaud Institut National de Recherche en http www cecill info licences Licence CeCILL C Vl en html KKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK Ioa inter ml 4 2011 10 06 11 47 22 bearllau Welcome to Mica version 0 08a it Define an array of states val lt Inter value array abstr lt abstr gt lt abstr gt abstr lt abstr gt abstr abs abstrl Define events Notice event vehicule sense takes a boolean parameter Valves bool gt Inter
12. ng 4 Graph tdemrliier gt gt sering iile mnane curat Signature are definedinanew signature define signature block Functions output and input are used to add an event to the current signature These two functions can only be called withinanew signature define signature block OS CRE NEUTRE oes Sitevmst eG hoattine NONINS EEE Che tron oO a cuc mec uoles semis e EEE UL al mie e Cer lines cigna ur en terminates TRE definition OE EN STONES S VeleGebi nestle ne EEE EUM M SC NE CURE output e defines value e to be an output in the current signature valf outcput M IUe IUS input e defines value e to be an input in the current signature sempe SUR USE Systems and interfaces on signature g are defined within new system g define system and new interface g define interface blocks Function define interface returns a reduced interface Quat Slt AND E exi TE RS Qs ose evene en ens SU ES Ie pe Clore med Or eet eye teil Or C ES TOME rts ici walinew Ve ren Cum une Ce ICE RIRES SES UM ON Geet mine tes elec rele TE TUIS OMC ey Sse es uc ee nee I MEUS M EC 5 Mew Minteterece S SEAT CSN ENEMNCE FINALE TOM C1 ERA NES RACE Wich Slee ciics CTI va lew inter hace sure cu unit Ce ele Irene CE MMS MINE LOS Eq Cle tae loi ONE Sia TIES IOS ucdederameqEn erbe UE Munch E Function void is used to define the inconsistent interface Remark that the empty new interface g define
13. ng toolbox dot command e gmake only for Darwin and most likely Solaris e Ocaml version 3 12 or later compiles on earlier versions but has not been thoroughly tested To compile this software change to folder src and proceed as follows l CopyfileMakefile config generictoMakefile config 2 Edit fileMakefile config and set the installation folders 3 Run the following make or gnake command 4 This produces the following libraries and interactive commands e mica cma Ocaml bytecode library e mica cmxa and mica a Native codee library ocaml mica Ocaml toplevel linked with the mica library e mica the interactive environment 5 Installation is done as follows or as follows if superuser administrator privileges are required The Mica library consists in several modules Modules that can be used directly are listed below Other modules are technical and are not covered in this manual Inter Mica interactive environment commands and functions Display Displays systems and interfaces using Graph Viz Pattern Library of modal patterns using regular expressions Objexpr Regular expressions on heap objects and mapping to modal interfaces Regexpr Polymorphic regular expressions Mi Modal interface algebra System System algebra Signature Signature algebra Modal Algebra of modalities Orientation Algebra of I O orientations Equiv Equivalence relations Rel Bina
14. on ur e E r eea TT Systems can be mapped to interfaces and vice versa Mappings between interfaces and systems E E ER G ace or TS en mape eE ermino Ooy emn na org nera SE C e Payee e te ail bs OO Een HE SO m valfin er cocer Ea Im E mE qum e wi Gena line lementi tron i Ra eo Err o EE anera EGE E RE Vel uL CU DN liemnentat onk inter CROSS sos cen Ve lite implementation REE move Een The parallel composition of systems can be computed with the following function The parallel 10 composition of I O incompatible systems whenever a system is ready to send an event while its peer system is not ready to receive this event produces warnings CompeoSLelon Cperavor Onmeystems parallel mil m computes the parallel composition of mii and mde val parallel system gt system gt system Composition operators on interfaces Function wimply is the weak implication operator introduced in G Goessler and J B Raclet Modal Contracts for Component based Design SEFM 09 The optimistic parallel composition produces warnings whenever incompatible state pairs are reachable in the product interface Composition operators eR een umet ron E computen Ene co LR T Ol Interfaces eend sz val conjunction interface gt imverface gt interface A product slesZ computes tne product Or intertaces Visi and E val product interrace gt ER s e Interface Je Z E lentes Ss S computes the residuation
15. ot els NN S Vel guotient n inte face Inter rgo litem dee es Heer To ols rent Ox es que er le Comemuss EIOS eon exe EO des TEES TLOTDIEUE oem EEE E TE BIOS a by interface b It is the largest x such that x is compatible with Sean produ t Dpi etg mese a valt ompart Keto oti enie iSc ec EI e IC Ee A gt RT RI siess2 complies the tweak implication ots sioe val wimply interface gt interface gt interface eontra t g al Our ombre ti IR ler lel val contract gt interface gt interface gt 1Interitace Poteet Reprise hers so S GO EM EN eoe mi ET ke onp eron of interfaces sl and s2 ox Werk Jeeves ESI 8 ucc Se Mics ies gt usce Satisfaction refinement and consistency can be checked with the following functions Violation of satisfaction or refinement produces warning messages explaining why the relation does not hold Relations on systems and interfaces 11 satisfies m s decides whether system m satisfies interface s Val satisfies system gt rntestace gt bool refines sl s2 decides whether interface sl refines interface s2 val refines interface gt interface gt bool MI Necemcu ciem Nec rente EIE I concessus pi VENTES SC OS TS CONCLUE EMTEC CMS Couplers S ENS RENE e RACE sl SC CMOl ete puce compile cM Sq e P ooo t5 qms ER EUR EN SU Chioeks W ste IT DE exc Ie as S E cw puc E Nerv ME ESI c Pe Interfac
16. ry relations on heap objects Ltr Labelled transition relations Ltf Labelled transition functions Enum Sets defined by extension Mmap Curryfied mappings from pairs of heap objects to any type Mapping Mappings from heap objects to any type Heap Heap of objects with hashing and structural equality Their dependency partial order relation 1s as follows zi The Mica interactive environment For a detailed documentation of the mica commands and functions see the description of the Inter module below but also in file inter mli inthe src folder The Inter module Module Inter defines the commands available in the mica interactive enviroment Whenever an error occurs at runtime an exception Error is raised The parameter is an error message Ce gero Err or SES e SOON IREM ENE TN ET iere Oe OXENETU DEL on exception Error of string In a nutshell the tool computes on five types of objects e type value is used to define states and events e type signature is used to define I O alphabets type system is used to define systems component implementations Systems are parameterized by a signature type interface is used to define modal interfaces component contract abstraction or behavioral type Interfaces are parameterized by a signature e type expression is used to define modal regular expressions a convenient way to define interfaces type value heap elements type valu
17. sense true vehicule sense true aN ACL SO EAN ES RACE dur Slick ge TOUS SENTE EST av Cee meguesic T 15 let sigma entry gate ticket new signature input vs truel input vs false TOU CE Outpt ti QUE Ed input Cg OUEPUE GO INSIDE eC Mme MS UE let itf entry gate ticket DEMI STATE Senec cede dese o EE IE Te Tee ga NE may c 0 vS false g 0 may g 0 vs true qg 1 Me g O are cs may g I v3 false g 0 ma a eee a may ge 2 vs false g D na a ie o ue USE oA ME o Sr May gq 3 vs false g 4 noe eC el 2 Mace o E mase C74 recle 05 may q 4 v gt true qe mar g A er oa E may g 9 vs false g 0 mase G15 GO 6 mar Gg ete Ce UE may g o vs faloa T SOINS OR SL TS must SL EC S Mes Me TN vs true g on RSEN NE EM oe ih derine iver hace d Pdi plaa ta elias bie Sie Ce Sie oe abies Vee ay VO erie palo ec Compute the conjunction of the three interfaces let itf entry gate Conde LOI Conjunction RER cs Pe Onte Oe eques Met a E ele kewry Checks whether the conjunction is consistent i 1S COMSiLS Sime Ie S Displays the conjunction figure below i Cols ole a der Wu rues Cece ale Sites cue cc Prints heap statistics 16 vehicule sense false vehicule sense false vehicule sense fase ticket request f vehicule_sense true vehicule_sense true ticket_request ticket_request
Download Pdf Manuals
Related Search