Home

Requirements Analysis Tool with Synthesis - RAT

Contents

1. Y GW gt F a amp amp F r Y lr gt F a amp amp FO r gt F a r Vv Fla Witness Counterexample Status Result Witness Analysis Figure 25 Witness for property G r gt F a amp amp F r X BRST es pX 2 Assurance Simulation Realizability File Edit View Help Bou e Open Traces Property G tr gt F amp amp Fir Property Simulation Signals 7 GW gt F a amp amp FO Gl r gt F a Y r gt a r Vv F a Witness Counterexample Status Result Witness Analysis Figure 26 Witness for property G r gt F a amp amp F r Asking for a new witness produces a trace illustrating that our requests are satisfi able Figure 28 We have used all elements of the Property Simulation interface so far and now it is up to you to explore the property and the potential of Property Simulation on your own To give you some initial direction we would like to suggest to enhance the property to allow an acknowledge only on a request or to limit the length of an acknowledge to one time step 1 4 Property Realizability and Synthesis in RATSY This section illustrates the RATS Y Property Realizability and Synthesis features
2. lt gt Witness Counterexample Status Result Witness Analysis Figure 24 Witness with request for property G r gt F a The derived trace illustrated in Figure 25 however unveils that we have got some thing wrong as the tree structure does not fit our intention By the investigation of the tree structure we uncover that we have forgotten two brackets We have to put the G part of the property into brackets otherwise the logical and binds the F r to the implication part and not to the globally part We add additional brack ets to the property to gain G r F a amp amp F r By asking for a new witness we recheck the property and are satisfied with the presented trace and evaluation Figure 26 Now we want to check if a single of the two acknowledges conforms to the prop erty Again this might be obvious for our example but it might not be obvious for a more complex one Thus we shape the trace by editing the waveform We fix the values of signal r to the values of the trace and signal a to true for time step one and false for the remaining time steps Figure 27 RATSY Requirements Analysis Tool RATSY Users Manual e 19 with Synthesis X BRS ESE File Edit View Help kA Assurance Simulation Realizability Dou M Open Traces Property G r gt F a ea FO Property Simulation Signals r a
3. 20 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis X Bee eee ox File Edit View Help SoG p Y Open Traces Assurance Simulation Realizability Property G r gt F amp amp FD Property Simulation Signals r a Evaluation T G r gt F a amp amp F r Gl gt Fa r gt F a r F a a Fir r gy Witness Counterexample Status Result Outdated Analysis Figure 27 Shaping the trace X Ee o File Edit View Help Open Traces Assurance Simulation Realizability Property G r gt F amp amp F A Property Simulation Signals r a Evaluation T G r gt F a amp amp F r Gl gt Fa 7 r gt F a r F a a Fir r g3 Witness Counterexample Status Result Witness Analysis Figure 28 Witness for shaped trace request For using the Realizability feature the enhanced version of NUSMV 5 is re quired For using the Synthesis feature the command line tool MARDUK is re quired See Section 3 for details Realizability Problem Informally the Property Realizability problem can be described as follows All signals are divided into
4. RATSY uses external tools to check properties for Property Assurance Simula tion Realizability and Synthesis In particular currently it relies on the NUSMV and VIS model checkers that are written in Posix C language Furthermore it uses the MARDUK tool written in Python which in turn uses some functions from NUSMV via a wrapper The tools are called and used by RATSY as external pro cesses and are kept separated from RATSY by an abstraction layer called Stub that exports a standard interface The MARDUK tool is partially tighter integrated with RATSY since both are written in Python Especially the Game features rely on this integration RATSY is based on several other software entities that affect its software archi tecture The picture in Figure 44 shows the main set of layered software entities which RATSY relies on The layers depict the dependencies among the entities as higher parts depend on lower parts At the top is positioned the RATSY Application gray shaded to make it clearly distinguishable from the other parts The single parts are described in the following from the bottom to the top RATSY Requirements Analysis Tool RATSY Architecture e 41 with Synthesis RATSY Application MVC amp Observer Infrastructure PyGTK Bindings rere Toolkit Python Library NuSMV ia Operating System amp Runtime System Libraries Figure 44 RATSY Software parts and collocation Operating System amp Runtime Sy
5. with Synthesis Table of Figures Figure 1 Figure 2 Figure 3 Figure 4 Figure 5 Figure 6 Figure 7 Figure 8 Figure 9 Figure 10 Figure 11 Figure 12 Figure 13 Figure 14 Figure 15 Figure 16 Figure 17 Figure 18 Figure 19 Figure 20 Figure 21 Figure 22 Figure 23 Figure 24 Figure 25 Figure 26 Figure 27 Figure 28 Figure 29 Figure 30 Figure 31 Figure 32 Figure 33 Figure 34 iv e Table of Figures RATS Y Main window 0 cccececeecsecesereceeneceeseseensonenes 2 RATS Y New project wizard cc ccceeeeeeeeeeneeeeeeeeeaaenees 2 RATS Y New project wizard project data 1 0 0 ee 3 Property Assurance main window c seeeeeeeeeeeeeeeeeeees 4 Creating signals requirements ceceeeesseeeeeeeeeeneeeenees 5 Creating possibilities and assertions cceeeeeeeeeeneeeeeees 6 Verification panels i a a 7 An example of trace visualization eeeeceeeeeeeereeresrereree 7 An example of trace visualization eeeeccceeeeereeereerrreree 8 Editing a categoTy s sviiivcccsveesivecvecieeececsesvestveaeouaeecaeenee 9 Editing a ACE 2 ccve ccd eccneccsusecivecstvecieeecasccoveestvedneeeaasecsteese 9 Counter initial specification ccc ceeeeeeeeeeeneeeeeeeeeeeee 10 Counter checking an assertion reene 11 Counter fixing the specification ccc eeeeeeeeeeeeeeeeeeee 12 Counter checking a possibility 0 0 0 eeeeeeeeee nena 13 Counter traces of the S
6. H Inc SNF Partition SBMC F Depth 30 a z Cone of Influence 7 Dynamic Reordering Loop AllLoops zi Figure 7 Verification panels Traces and their management The results of verification checks are shown as traces which are shown as new tabs beside the Output tab as depicted in Figure 8 X GASES RPX File Edit View Help New Open Save Traces Assurance Simulation Realizability Signals gt Requirements 7 66 Name Type kna Notes amp Name Kind Property Notes a boolean S f always b boolean S a b next c c boolean S r G eventually a amp amp Ib amp amp next b Property Assurance i may Possibilities Assertions A Check 4 8 Ei ame sans ropery Joes Sa TecinlogySDDTedloy Fi posso v eventually c Solver MinisAT v Clinc 1 SNF C samc Depth 30 z Loop All Loops Y C Consistency V Checking outcomes Name Trace_6 Dep r0 r1 poss0 Cat New trash Figure 8 An example of trace visualization Each trace has a name and is connected to the requirements and the possibili ties assertions it has been generated from i e those that were selected to perform the check of which the trace is the result These
7. ferent sessions and of saving the results of the work performed from session to RATSY Requirements Analysis Tool RATSY Users Manual e 1 with Synthesis X A o x File Edit View Help Beum e 8 New Open RAT v 1 2 Atool for Requirements Analysis Copyright c 2005 by ITC irst Copyright c 2005 by Graz University of Technology Q Quick Start To start a New Project dick New To load an Existing Project dick Open Figure 1 RATSY Main window session With Property Simulation such a feature could seem less relevant but the value of having the possibility of saving simulation sessions i e the properties simulated and the connected traces shows clearly if we think of long time con suming work sessions and of the importance of having a quick reference to their results Through the menu File or the command New in the tool bar it is possible to access the wizard for the creation of new projects shown in Figure 2 select the kind of project and specify the details of the project entering the data in the fields shown in Figure 3 X ET o Specify the initial project type Property Assurance Property Simulation Realizability Property Assurance allows for Note It will be possible to switch among the project types at any time 8 Cancel 4 P Forward Finish Figure 2 RATSY New project wizard As a result of the integratio
8. SSION ceceeeeeeeeeeeneneeeeeeeeees 13 Property Simulation Main Window sseeeeeeeeeeeee 14 Property Simulation Evaluation Analysis Window 16 Create a project for Property Simulation 1 0 00 17 Property Simulation Start Window eeeeeeeeeeeeeeeee eee 17 Witness for property G r F 4 sisciccecsisuscerdeabieenssdeondes 18 Analysis of trace for property G r gt F a ecese 18 Ask for a request on signal r ssesssereresereresesssrereresrsereress 19 Witness with request for property G r F a ceecee 19 Witness for property G r gt F a amp amp F r aecccsscseee 20 Witness for property G r gt F a amp amp F r ceee 20 Shaping the tracers iioi an RERA 21 Witness for shaped trace requeSt eceeeeeeeeeeeeeeeeeeeenees 21 Specification of an environment signal in RATSY 22 Specification of a system guarantee property in RATSY 23 The Realizability window in RATSY ecce 23 The Realizability window in RATSY nece 24 Create a new automaton 0 cece eeeceeneeeeeeeeceeeaneeeeeeeeeas 27 Edit the properties of a state in the automaton 27 RATSY Requirements Analysis Tool with Synthesis Figure 35 Specify the transition condition for an edge 28 Figure 36 The main window of the automaton editor ee 29 Figure 37 The Game window in RATSY cccceseeeeceeeeeneeseeeeeeee 31 Figu
9. Tool with Synthesis which are not available via the graphical user interface of RATSY If you want to start synthesis directly from inside RATSY click the Synthesize button and select a file to store the synthesis results The following options for controlling the synthesis process are available on the lower right hand side of the window The synthesis process will also respect the options for dynamic reordering which can be set right below the Check Realizability button Before starting the synthe sis process the desired mode should be selected At present the following modes are available 1 COFACTOR A cofactor based approach presented in 3 and the BDD Restrict operation of the CUDD package is used to compute output functions from the strategy 2 IRRSOP This mode is based on the Minato Morreale algorithm for com puting irredundant sums of products 7 combined with a cache of already implemented subfunctions to find deterministic output functions 3 FACTOR This mode is a generalization of the IRRSOP mode Instead of single literals arbitrary Boolean functions are used in each recursive step This mode is experimental 4 OLD This mode is a legacy mode from a previous release It is basically the same as the COFACTOR mode except that the output file is directly dumped from the CUDD package This might save a little computation time but it limits the output format to BLIF After setting the mode one of three
10. a EERE EEA EUEN vi 1 RATSY Users Mamtiall oi si co csuscucesuee scandscteodasiunadesitdestncueetucandneanscsedeatsocs 1 Li Running RATS Y sscsica dines cctac teats madeedacuiad eancon nays ataaatnnaanacetiasads 1 1 2 Property Assurance in RATS Y oo cee eeeecceeneeeeeeeeeaeaeeeeeeeeeaaees 3 The Matt Wind OW iadsacscetstsccad covedostsavicotsaesnsdeateunastsadiematdaccedancens 4 Traces and their management sciencia 6 An Example peresen rannen enna E a ENEN ER 9 1 3 Property Simulation in RATSY eesrnsscrsrisssiisisciiiiiriiiiia 12 The Mam Wind OW va ssisaceeagctiatcsacecmtendacwiad Mua diendieadavanecniinaedate cate 14 The Analysis WindOW iis s2sccsescheadesesasseiasdsdasdecetactsesesoceuieasceaiettes 15 An example ivciiccctssievislvecsiees aedecs teint cane EA E E K N 16 1 4 Property Realizability and Synthesis in RATSY 20 Realizability Problem cresine aniei iaia 21 Specifying a Realizability Problem sesssersnrsicsriscissisiinisiiia 22 The Main Window ceceecesesseeecceeeeueeeeeceeeaeeeeeeeeeaaaaeeseeeeeaaens 22 SYMCMESIS iic aussesdeahGaoahcsaduonsidencedenduawsdetendensladdined ssdennetuaseedaedors 24 The Automaton Equtor isigs isis ccdsiccnteagenadaesisineneawninidadenatineions as 26 1 5 Simulating and Debugging Specifications using Games 30 How to play a Game sissano i o aieiaa Ea 30 The Game LoS Window casir aE macdenegans 32 Integration with the Automaton Editor cc eeeeeee
11. amp amp error 0 startup_failed boolean E environment could not start up v sys tran 0G never g0 1 amp amp g1 1 go boolean S resource granted to entity 0 vsys tran 1 G always error 1 gt gO 0 amp amp g1 0 gl boolean S resource granted to entity 1 v sys fairO G always eventually rO 0 gO 1 error boolean S something went wrong vsys fairl G always eventually rl 0 g1 1 di_stateO boolean S venvfair A always eventually TRUE di_state1 boolean S design_intento G di_stateO 1 dead boolean S lt E J lt gt Automata ox Notes a simulation run Figure 41 The new specification containing the desired behavior The play engine is reset with the button Stop and a new game with the enhanced specification can be started by clicking Start again The tool finds out that the en hanced specification is unrealizable so it starts a countergame in order to illustrate the cause of unrealizability It first minimizes the specification The tool says that the specification is still unrealizable if the system can choose the value of g1 com pletely arbitrarily in every time step It furthermore states that the specification is still unrealizable if the system does not have to fulfill sys fair 1 eventually a grant for entity 1 and sys tran 0 never more than one grant The countergame is played on this simplified specification where gl sys fair 1 and sys tran 0 have been removed Next the tool computes a counterstrate
12. an assumption on the behavior of the environment or a guarantee on the behavior of the system For instance Figure 30 show the RATSY wizard to specify the system guarantee always forall M in 6 5 v M amp amp inc gt next v M 1 The Main Window Once all the signals and all the requirements have been inserted in the RATSY project it is possible to move to the Realizability window where the button that performs the check of realizability for the selected properties can be pressed to start the check for realizability Figure 31 shows the Realizability window with an example of realizability problem The Check Realizability button on the right in the Realizability window of RATSY activates the realizability checks The result of the check is shown in the left text area In this particular example the specification is unrealizable because 22 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis Edit an existing requirement Name RI Property always forall M in 6 5 11 indent V M amp amp inc gt next v M Automaton Name Kind Guarantee Assumption Notes leach inc is immediately followed by an increment of v cance Box Figure 30 Kind Notes The input signal for incrementing the value of the counter The input signal for Name Type inc boolean E k Requirements amp N
13. different output languages can be selected BLIF Berkeley Logic Interchange Format Verilog and HIF HDL Intermedi ate Format Below the mode and language selection box some more options about BDDs are available The first checkbox lets you enforce a reordering of the BDDs after reading the specification and creating BDDs for all assumptions and guarantees It is recommended to leave this option turned on as it usually short ens synthesis time The next option enforces a reordering after the strategy has been synthesized The third option will delete the strategy BDD and also trigger a reordering once the output functions have been determined It is recommended to turn the latter two option on in BLIF mode and turn them off in the IRRSOP modes In IRRSOP mode output functions are not represented as BDDs any more so reordering will not improve synthesis results but just take time The next op tion enforces a transfer of all BDDs that represent output functions to a new DD manager before they are dumped into the output Experience showed that turning this option on slightly improves synthesis results at very little extra time This option is only available in BLIF mode The reorder method for forced reordering may differ from the one used for dynamic reordering Experience shows that using one of the converging methods is preferable Finally it is possible to choose between two different encodings of the jx state variables These varia
14. dot and game_data graph_with_signals dot The latter contains the signal values that make a certain state transition possible the former does not Pictures of the graph can be produced with the DOT program by typing for example dot Tpdf graph_with_signals dot o graph_with_signals pdf in a shell opened in the directory game_data Detailed information to the graphs is written into the file gane_data graph info This file contains the signal values corresponding to the different vertices of the graph The current state of the play in the graph is displayed in the waveform labeled with state in graph of the input trace For larger specifications the graph tends to become huge Huge graphs are no real help for the user so their computation is aborted if they exceed 100 vertices With the checkbox in the Game window graph computation can be disabled completely Special Waveforms The input trace in the Game window contains some wave forms that do not represent input signals The special waveform state in graph contains the current state of the play in the graph as already explained in the previ ous paragraph The waveforms labeled with ix and jx show the memory content of the counterstrategy as defined in 6 The value of ix gives the index of the fairness constraint of the environment that will be fulfilled next The value of jx gives the index of the fairness constraint of the system which the environment tries to evade Thus you can co
15. in Computer Science pages 364 380 Springer 2006 PROperty based SYstem Design PROSYD http www prosyd org 2006 Accellera Property Specification Language Reference Manual Version 1 01 http www eda org vfv docs psl_lrm 1 01 pdf April 2003 RAT Requirements Analysis Tool http rat fbk eu RATSY Requirements Analysis Tool References e 53 with Synthesis
16. including possible changes at the interconnection of the trace and the transition from the last state to the first state of the infinite part The graphical concept uses a tree view for organization of the visualization and offers a close button at the bottom to close the window The tree view shows the coverage Statistics for each part of the property and the controls to request features The first column contains the name of the part followed by nine columns to illus trate the coverage information For each part there are columns labeled 0 and C corresponding to the numbers for false 0 true J and evaluation result changes C The three sections for the finite infinite parts and the whole trace are distinguished by the used background colors The sections for the finite and infinite parts use the same colors used for the waveforms light grey and dark grey The section for the whole trace uses a very dark grey Additional four columns offer the option to request features for the next trace You can request a sub formula to evaluate a property eventually to true F globally to true G finally to false F 0 or G 0 A green zero for a request indicates that there is no request for the next trace whereas a red one indicates a desired request Pressing the right mouse button on a value produces a pop up window enabling to set or unset a request Conside
17. of each trace in the main window as shown in Figure 8 Clicking on the button Traces in the tool bar it is possible to access the window of the trace manager as shown in Figure 9 which allows the user to manage traces by editing the associated data moving them from a category to another category deleting them creating new categories and editing the data connected to categories DX CEE o Categories p z e Selected Traces show category category of those traces that have been just created PST ESS COTES I See pI ENTE Tes OT Up ae Veep ee ri Notes This trace has no notes Dependencies are r0 r1 possO History 00 Added to category New P Name Step1 Step2 Step3 a E gt M have been deleted Traces 9 Trash Contains the traces that have been deleted gt Trace_0 Show Name Category Name step1 Step2 steps Trace_6 New Trace_0 Trash R Trace_1 Trash gt a Trace_2 Trash e Ss Trace_3 Trash Trace_4 Trash p maei Name step Step2 Step3 a eae eee A J c Figure 9 An example of trace visualization At the top left corner of the trace manager window the list of categories is shown where each category has a name and a Description it is possible to select more than one category and on selection the contained traces a
18. of the Property Simulation interface On the upper left you can see a multi row text entry window where you can enter your property The various lines are combined to a single property thus you may split your property to several lines for a better overview The middle section of the Property Simulation window consists of two widgets showing waveforms The upper one illustrates the derived example behavior using waveforms The different waveforms illustrate the signal values for every time step in the trace The whole trace is determined by the finite part as prefix completed by an infinite repetition of the infinite parts The background color indicates whether the value is in the finite or infinite part of the trace Light grey corresponds to the finite part and dark grey to the infinite part You may select a single signal to highlight its waveform there is no further impact of such a selection The trace signal view offers the possibility to request features for the next trace A click on the right button of your mouse on a step of the trace produces a pop up window offering the following requests 14 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis e Insert timestep Another time step is entered just before the one you have clicked on The default value is Do not care which means that you don t have any preference for the value in the next trace e Remove timestep A given time step is removed in the next tra
19. s 5 error gt all assumptions are fulfilled but not all guaratees s di_state0 R 4 z z i di statel Show Resul Show Operations Show Help Figure 42 The countergame containing the countertrace Figure 43 shows the Automata window in Step 2 of the play It contains only the automaton representing the design intent which we specified earlier In Step 2 we are in the state V2 We have that startup_failed 1 so we can only set error 1 in order to stay in V2 which is accepting Setting error 0 would bring us to the state R2 This step is non accepting and it cannot be left any more if not the environment sets startup_failed 0 which it does not following its countertrace Clicking on one of the yellow edges in the Automata window makes rror lorerror 0 in the Game window The countergame helps you to understand the conflict between the specified design intent and the rest of the specification that is why the enhanced specification is unrealizable The elimination of the problem is up to you as there are typically various solution You could allow grants to be given on error you could restrict the fairness guarantees sys fair 0 and sys fair 1 to cases where error 0 you could add an assumption that forbids that startup_failed 1 forever etc 38 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis 3 gt B gt o gt EE oS Automata Step 2 Name Notes istartup_failed Fi
20. specification RATSY Requirements Analysis Tool RATSY Users Manual e 23 with Synthesis realizable Figure 32 Name Notes Realizability Num Realizable Requirements a g 33 Check Realizability 1 no RLR2 wi Se 2 yes R1 R2 R3 Partition Threshold x l3 yes R1 R2 R3 R4 R5 fairness _sys fairness_env Synthesis number 3 i Dynamic Reordering Selected requirements were found realizable Requirements were R1 R2 R3 R4 R5 fairness_sys fairness_env ails x Synthesis result stored to users 12398 ghofferek work devel_RAST rat counter blif Synthesis options were dyn dyn_reorder_method sift r1 r2 kill transfer functions reorder_method sift_converge gt Synthesize Synthesis mode BUF mi Reorder BDD after reading configuration il Reorder BDD after synthesis Kill strategy when no M longer needed and reorder BDD SZ Transfer output functions to new BDD mananger Reorder method for forced reordering _ St converge Encoding of jx state vars Binary One Hot Signals op Requirements B 8S Name Type Kind Notes t Name Kind Automaton Property Notes la always prorat min 70 0 Vv does NUL Change ir no ie ana UN i Mins s v M amp amp tinc amp amp dec gt next v M dec commands are issued inc boolean incrementing the value L of the counter R5 G v 0 Initally the counter is 0 The input sign
21. two disjoint sets uncontrolled environment signals and controlled system signals Similarly every requirement belongs to one of two sets the assumptions and the guarantees At every time step the environment variables are set to some unknown beforehand values and then the system decides RATSY Requirements Analysis Tool RATSY Users Manual e 21 with Synthesis values for its variables Assuming that the assumptions hold the task of the system is to satisfy the guarantees If the system is able to do that for every possible behav ior of the environment the specification is Realizable Otherwise the specification is Unrealizable For a detailed definition of the Realizability problem see 5 Specifying a Realizability Problem As was told in Section 1 2 the distinction of signals in System and Environment as well as the distinction of requirements in Assumption and Guarantee is important only for Property Realizability Thus now a user has to specify explicitly whether a signal is an environment signal or a system signal For example Figure 29 shows the wizard to specify an environment signal inc of type boolean Similarly a Xo TT o gt Create a new signal Name inc Kind Environment O System Type Boolean Other gt Editor Notes The input signal for incrementing the value of the counter 3 Cancel 2 ok Figure 29 Specification of an environment signal in RATSY requirement describes
22. RATSY Requirements Analysis Tool with Synthesis Version 2 1 Authors Roderick Bloem Roberto Cavada Alessandro Cimatti Karin Greimel Georg Hofferek Robert Koenighofer Alessandro Mariotti Ingo Pill Marco Pensallorto Marco Roveri Viktor Schuppan Richard Seeber Simone Semprini Andrei Tchaltsev and Martin Weiglhofer 2005 2009 2010 by FBK irst and Graz University of Technology Notices For information contact RATSY ratsy list fbk eu The first version of this tool RAT has been developed within the PROS YD European project contract number 507219 http www prosyd org The current version RATSY has been created within the COCONUT European project contract number 217069 http www coconut project eu within the DIAMOND European project contract number 248613 http www fp7 diamond eu and within the Provincia Autonoma di Trento project EMTELOS The information in this document is provided as is and no guarantee or warranty is given that the information is fit for any particular purpose The user thereof uses the information at its sole risk and liability Copyright 2005 2009 2010 FBK irst and Graz University of Technology All rights reserved ji e RATSY Requirements Analysis Tool with Synthesis Contents Contents ioneina eiaa eE EEEE NEEE ETENEE EES EEN EEEREN ENEE iii Table of Figures oavenronnroircinicirrii en e EE EEEE EERE iv List f Tables soper tenn pia eaen eae bae Pea E EEEE
23. View Controller to present the options to the user and to allow the user to modify the options Those entities that instead do not need to be shown e g the stubs will be mapped directly down to one class or to a set of classes In the following the software entities depicted in Figure 46 are detailed Application The application is the top level entity When the RATS Y executable file is run a triple Model View and Controller of this entity will be instan tiated and connected each other and RATSY will finally enter in the main event loop to handle user interaction and events Application Options This entity is a container for application s options For ex ample tools paths and other general purpose options should be localized within this entity At the moment this entity is empty and there is not an associated View for it Project This entity represents a RATSY project The project s model contains most of the application logic meaning that most of the application s models are contained within this model The view is embedded within the applica tion s main window whenever a project is created and it is constituted by a large number of sub views corresponding to the contained entities Project Options This entity is a container for the project s options Similarly to the Application Options entity this entity is currently empty and there is no associated view Signals This entity contains the set of signals used by P
24. a Notes Name kina Property Notes The input signal for always forall M in 6 5 each inc is immediately v M amp amp inc gt next v M 1 follewediay inc boolean E incrementing the value IRL G of the counter f The input signal for dec boolean E decrementing the lt I R2 G value of the counter v 6 6 S The value of the counter an increment of v always forall M in 5 6 each dec is immediately as i re followed by v M amp amp dec gt next v M 1 PEES inc and dec never occur simultaneausly v R3 A never inc amp amp dec Property Assurance Possibilities Asserti Possibilities soa Bact Check Consistency 28 6 Sat Technology BDD Technology always forall M in 5 5 v does not change if Solver MiniSAT liv Inc SNF v M gt v M until inc dec there are no inc and dec L SBMC Menth 30 let ma Name Trace_1 Dep R1 R2 R3 A1 Cat New o Trash Move Figure 13 Counter checking an assertion Once A1 has been entered we can check it against all the requirements and get the result shown in Figure 13 the assertion is signaled as failed by a red bullet next to its name in the Assertions table and a trace showing a counterexample to A1 is created and shown at the bottom of the main window No
25. ace_5 New El Trace_0 Trash Default This is the default category for traces Out of Date Contains the traces whose dependencies might be no longer consistent Trash Contains the traces that have been deleted gt Trace_o EI RATSY Requirements Analysis Tool Figure 16 Counter traces of the session with Synthesis RATSY Users Manual e 13 1 3 Property Simulation in RATSY This section illustrates the RATSY Property Simulation features Some general GUI features will be introduced followed by explanations of the main and analysis windows and an example scenario for a simple standard property The Main Window When enacting Property Simulation in RATSY you will see the RATSY main window to change to Property Simulation mode as illustrated in Figure 17 Please note that the user is able to switch the mode at any time using the switch controls in the upper right of the main window X ERG ec ox Eile Edit View Help Open Traces Assurance Simulation Realizability Property G r gt F Property Simulation Signals Step1 Step2 step3 a Evaluation step1 step2 steps F Gir gt Fa 7 n gt Fa r F a a x t gt Witness Counterexample Status Result Witness Analysis Figure 17 Property Simulation Main Window In the figure you see the three main sections
26. al for p M fairness_sys G G F TRUE dec booleanE decrementing the value a ti faimessenv A G F TRUE 5 Automata d Figure 32 The Realizability window in RATSY A set of assumptions and guarantees is internally converted into an equivalent NUSMV game structure and depending on the generated game structure the cor responding check algorithms are invoked with the help of the enhanced version of NUSMV 5 The generated game structure is printed in the log tab as to allow the user to inspect it Note that such a game structure may have fresh variables introduced during conversion If the tool is not able to convert a RATSY speci fication into a NUSMV game structure an error message with the subexpression causing the problem is printed out Synthesis For realizable specifications an implementation can be automatically synthesized Synthesis works according to the algorithm presented in 10 To perform synthe sis RATSY relies on the command line tool MARDUK which it calls as an exter nal process Since synthesis can take a very long time for larger specifications it might be preferable to invoke the MARDUK tool directly from the command line in order to have it run in background and independent of the graphical user interface MARDUK is able to read and process RATSY project files Also the command line tool provides some advanced and experimental features and options 24 e RATSY Users Manual RATSY Requirements Analysis
27. ame Kind Automaton Property always forall M in 6 5 V M amp amp inc gt next v M 1 always forall M in 5 6 Jp Re 26 V M amp amp dec gt next v M 1 MRL G Specification of a system guarantee property in RATSY Notes each inc is immediately followed by an increment of v each dec is immediately followed by an decrement of v Automata Name Notes Realizability Num Realizable Requirements p no RLR2 Realizability number 1 Selected requirements were found not realizable Requirements were R1 R2 gt Checking outcomes amp Check Realizability Partition Threshold v W Dynamic Reordering sift gt Synthesize Synthesis mode BLIF Reorder BDD after reading configuration Si Reorder BDD after synthesis Kill strategy when no WV longer needed and reorder BDD Transfer output functions to new BDD mananger Reorder method for Sift Convert m forced reordering g Encoding of jx state vars Binary One Hot Figure 31 The Realizability window in RATSY the system may force the violation of the guarantee requirements by setting both signals inc and dec up To avoid such behavior we can add an assumption re quirement never inc amp amp dec With this assumption the specification becomes The cause of unrealizability may not always be so obvious See Section 1 5 to learn how to debug an unrealizable
28. ble specifications are checked for satisfiability first The result is written to the Game Log window If a specification turns out to be unsat isfiable you do not have to play a game in order to understand the problem You can also use Property Simulation to learn why no trace can fulfill the specification This may lead to simpler explanations However as unsatisfiability is just a special case of unrealizability the countergame can also be used to explain unsatisfiability If undesired the SAT check can be deactivated with the corresponding checkbox in the Game window Minimization All output signals and guarantees that are irrelevant for the unre alizability problem are removed from the specification before a counterstrategy is computed A guarantee is irrelevant if you cannot fulfill the specification even if you would not have to fulfill this guarantee A signal is irrelevant if you cannot fulfill the specification even if you could choose the value of the signal completely arbitrarily in every time step without any consequences for other signals Irrelevant guarantees and signals are not included in the game This helps you focus on the actual problem The irrelevant guarantees are deactivated in the table of require ments of the project Which signals are irrelevant can be seen from the Game Log window Minimization can be deactivated with the corresponding checkbox in the Game window Countertraces A counterstrategy is a strategy for t
29. bles store which fairness condition the system is going to fulfill next cf 10 for details The default value is Binary It is highly recommended to use dynamic reordering as it will greatly reduce memory and CPU time usage 3See http hifsuite edalab it for details RATSY Requirements Analysis Tool RATSY Users Manual e 25 with Synthesis Caveats There are two very common scenarios which can cause the synthesis process to terminate abnormally Due to limitations of the implementation the current version of RATSY does not specifically report the causes of abnormal termination in these cases Thus if RATSY reports that the synthesis process ter minated abnormally you should check whether one of the two following scenarios applies to your project First RATS Y can only synthesize specifications in Gen eralized Reactivity 1 format That means that at least one assumption and at least one guarantee must be a fairness liveness constraint If your specification violates this restriction you will see a message similar to the following at the end of the Checking Outcomes window Error The given specification is not a GenReactivity specification The game type is AvoidDeadlock If you see such a message you should augment your specification with a guaran tee assumption of the form G F TRUE to make it a GR 1 specification Second if one of your requirements causes a parse error the synthesis process will also
30. ce e Fix value to False In the next trace this value shall be false e Fix value to True In the next trace this value shall be true e Set to Do not care You do not care about the signals value at this time step in the next trace This option can be used to unset required values When you establish requests you will notice that the color of the trace for this signal and time step changes to red Red parts in the trace show that these parts are requested to be fixed to the current values for the next trace request You ll also notice that the status Value at the bottom changes to Outdated and the waveform color of the formula evaluation changes to black This means that the tree view for the Formula Property evaluation does not correspond to the trace anymore The tree view for the Formula Property evaluation beneath the Trace Signal view is not editable so you cannot shape the waveform here It illustrates and corre lates the single parts of the property to the trace For each time step of the trace the property and all its sub formulae are evaluated to true or false visualized by waveforms organized in a tree The tree structure is derived from the property to illustrate the dependencies between the parts of the property Use the tree view to make sure that the formula has been parsed the way you expected Relating the waveforms to each other shows how the different parts of the property interact with each other interpreted on the
31. ce this initial specification is entered by the user it is possible to proceed and check it for consistency i e checking that the requirements are not mutually con tradictory This can be achieved by selecting all the requirements by ticking the check box Consistency check and by clicking on the Check button in the con trol panel at the top Figure 12 shown the result of this check is positive the output from the verification engine shown in the tab Output reports that the run of the engine has completed successfully and no warning message is issued by RATSY As shown in the control panel this check has been performed using SAT technology with a depth of the problem equal to 30 and checking for all possible loop backs RATSY Requirements Analysis Tool with Synthesis Now that we have an initial consistent specification we can start analyzing it and check if it describes exactly the behavior we have in mind The first step can be that of checking that the value of our counter is always coher ent with the inputs received In particular we want to be sure that if no operation is issued the value of the counter does not change whatever the value is this is the meaning of assertion Al shown in the Assertions table in Figure 13 xa RAT DemoPropAssurance OXx File Edit View Help New Open Save Traces Assurance Simulation Realizability Signals gt Requirements 6s Name Te Tiin
32. cleared again i e set to don t care If some signal values are still don t care when the Next Step button is clicked these signals will be chosen arbitrarily by the tool With the button Prev Step the previous time step of the play can be edited again This is useful when you want to change some selection in some previous time step Note that the user selections for the current time step are lost when going back to the previous step You can put time steps into the infinite loop or put them back into the finite part by right clicking onto any signal in that time step and choosing the according menu item Only the last time step before the loop can be put into the loop and only the RATSY Requirements Analysis Tool RATSY Users Manual e 31 with Synthesis first time step of the loop can be removed from the loop This restriction avoids that you end up with more than one infinite loop or that the loop is not located at the end of the trace Time steps within the finite part are marked with light gray background Time steps with dark gray background belong to the infinite loop You can finish a play by clicking the Done button This causes the tool to analyze the play in order to find out the winner Furthermore explanations to this verdict are printed to make you accept that you have indeed lost the play When you finally click the Stop button the play engine is reset and a new game can be started by a subsequently clicking S
33. d state In order to specify transitions of our own we must first add signal names Right click in the list of signal names in the lower right part of the editor window and select Create Specify a name for the signal and click Ok The signal names that you specify here will be used to create the PSL formula representing the automaton Thus make sure that you only use names of signals that you created in your main project Oth erwise the resulting formulas will not work After you have created signals named reg and ack you are ready to add the edges to the automaton First we want to create an edge from s0 to s1 Thus first click the New Edge button then click on s0 and finally on s1 A new edge from s0 to s1 will be displayed Notice that the new edge is labeled true and that the dangling edge of s0 has disappeared to keep the automaton deterministic and complete We will label the newly created edge later after we have created all the edges we need Next create an edge back from s1 to s0 Note that you can add way points to edges After you clicked s1 click on an empty spot in the editor pane before you click s0 The new edge will pass through the point you clicked You can of course move the way point at any later time You can also add new way points to an edge by first selecting it with a left click and then clicking the middle mouse button somewhere on the edge RATSY Requirements Analysis Tool RATSY Users Manual e 27 with Synthes
34. d to as the connection is delegated to the controllers This is another variation with respect to the original MVC pattern as this implementation is intended to fit better with the PyGTK toolkit Controller Contains the actions that must be carried out when a view event re quires the interaction with the model s logic The Controller is always con nected to a single Model and to a single View making a sort of link among RATSY Requirements Analysis Tool RATSY Architecture e 43 with Synthesis these two separated parts of the pattern If a Controller can be connected to one Model the same model can connect more controllers at a given time The Observer pattern The Observer pattern connects the application logic to the presentation layer by allowing the latter to be notified when the former changes The Observer pattern is ofter used together with the MVC pattern and to a certain extent it may be considered as complementary as it handles the data flow from the model to the view whereas in the MVC pattern the communication goes generally from the View to the Model through the Controller This communication is carried out without making the model even know the exis tence of the view by using observable properties within the model and by defining observers over those properties The observers will be notified of any changing that occur to the observable properties In RATSY the MVC and Observer Infrastructure provides an impl
35. d you could use the binary distribution downgrade Swig to Version 1 3 38 or below or use the patched file NuSMV game NuSMVWrap dd ini swig 1 3 39 3 3 Running MARDUK No matter whether you use the binary distribution or the source distribution in order to run the MARDUK tool stand alone go to the marduk src folder and launch the file marduk py with your Python interpreter Make sure to set your environment variable LD_LIBRARY_PATH such that it also includes the directory NuSMV game NuSMVWrap nusmv clib This is necessary for MARDUK to find and use the NUSMV wrapper Run python marduk py h to display a help mes sage detailing the options and arguments of MARDUK In order to test whether the installation was successful you can run the script marduk src test_marduk sh 3 4 Licensing RATSY and MARDUK are distributed under GNU LESSER GENERAL PUBLIC LICENSE Version 2 1 February 1999 LGPL with the copyright held by Graz University of Technology and FBK irst See ratsy License for a copy of this license NUSMV http nusmv fbk eu is distributed under the same license with the copyright held by FBK irst only See NuSMV game nusmv README for details Since the same licence applies NuSMV sources are included in the source distri bution of RATS Y for convenience VIS is available under a different and even less restricted licence See http vlsi colorado edu vis for details The VIS sources are not included i
36. data allow to track the dependen cies among the traces and the other elements of the project for example knowing which requirements a trace depends on allows the system to signal it as out of date or no longer meaningful if some changes have been performed to one of the requirements the trace depends on In Figure 8 the trace shown is composed by an initial step followed by an infinite repetition of the second step i e a loop Loops are signaled by a little black RATSY Requirements Analysis Tool RATSY Users Manual e 7 with Synthesis arrow close to the name of the step they start from Color of steps changes to help depicting the finite prefix and the infinite loop in traces light gray for the former dark gray for the latter To ease their management and to reflect the typical use case of Property Assurance traces are organized in different categories among which the following system categories are provided New the category where traces generated in the current session are stored by default Default the category where up to date traces that have been generated in pre vious sessions are stored Out of date the category where out of date traces are stored a trace is out of date when some element in its dependencies have been deleted or modified Trash the category of traces the user scheduled for deletion A simple way of managing traces with respect to categories is provided by the buttons Trash and Move on the right
37. dy mentioned the interaction with the model checkers like NUSMYV and VIS is managed by a Stub a software entity that provides platform and Operating System independent support for running generic external model checkers The execution of a model checker is restricted to a stand alone thread that controls the model checker within a session The session is monitored and can be stopped at any time if the underlying Operating System supports process interruption Also the stub provides access to the session I O allowing to capture the model checker standard output and error and to control its standard input A stub execution is a sequence of events 1 The stub is initialized RATSY Requirements Analysis Tool RATSY Architecture e 45 with Synthesis A session is initialized The session is prepared setting of session options The session is run Session results are processed The session is de initialized SOY Ok oe ee NS The stub is de initialized The phases from 2 to 6 may be possibly repeated indefinitely A generic stub might control a model checker in any way either in batch mode in interactive mode or through its library In RATSY the stubs that control both NUSMYV and VIS use the model checkers in batch mode launching their respec tive executable files This is achieved by specializing the generic stub classes by implementing some interfaces and overloading some class methods that handles the execution of a single
38. e still holding gt The order of signals for specifying minterms corresponds to the order on the lower right side of the automaton editor window 28 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis B Automaton Editor arbiter Woe New State New Edge Align to grid Autocomplete Name Notes req Figure 36 The main window of the automaton editor down the left mouse button the label of the edge will be moved along the edge towards the target state If you move the mouse to the left the label will move towards the source state If necessary you can also zoom the editor pane at any time by using the scroll wheel of your mouse Once the automaton has been saved you can use it as a requirement To do so type the name of the automaton in the corresponding field in the requirements dialog cf Fig 30 After you typed in the automaton name the formula corresponding to the automaton will be automatically inserted into the property field Note that in this case you cannot manually edit the formula With the radio buttons below you can choose whether the automaton represents a guarantee or an assumption Click Ok to save the requirement Note that if you do changes to the automaton at a later time the PSL formula in the requirement will be automatically updated to match the latest version Furthermore you may use template parameters to reuse the same automaton several times Paramet
39. ed behav ior in the following way If the behavior of the environment matches the specified input trace then the behavior of the system must match the specified output trace Finally click Done and an automaton that accepts only the desired behavior is cre ated automatically and added to the table of automata in the project It can be added as an additional guarantee to the specification as described in Section 1 4 This eliminates the undesired behavior originally observed during the play Click ing Stop clears all data from the traces RATSY Requirements Analysis Tool RATSY Users Manual e 33 with Synthesis Once the Specify Design Intent mode is activated you cannot return to the Game mode again You have to click Stop followed by Start to start a new game Specifying design intent is only possible from a normal game but not from a countergame Additional Features for the Normal Game There is a special waveform jx in the output trace that does not correspond to an output signal It contains the memory content of the strategy according to 10 This memory content is the index of the fairness constraint of the system that will be fulfilled next You can simply ignore this row if you are not familiar with the work of 10 Additional Features for the Countergame Following 6 the countergame is integrated with additional features that make it easier for you to find out why the specification is unrealizable SAT check Unrealiza
40. eeeseeeeeeeeennees 32 Specifying Design Intent sic ciscc ccccssecasvesssecesesehecaianssigeccnaccaverenveats 33 Additional Features for the Normal Game n 34 Additional Features for the Countergame ceceeccesseeeeeeeeeneees 34 Bxam ple isc cctevectveecevvcnwseduvecseeceveenayedecessecevedayoaeceaiverversidodas 35 2 RRATSY Architecture essasi A 41 2 1 Architecture and Implementation Notes ceeeeeeeesseeeeeeeeeneees 41 22 Architectural Patterns 06cccciveccavecssvecsesenseecnweayecaeedserenverssvenss 42 The Model View Controller pattern cc ceeeeeeeeeeeaeneeeeeeeeeanees 43 The Observer patter i iccccsasecddushecesiesdeeiaatedusdecstantidadstgnamedvcenieties 44 2 3 SoftWare Struct e oaei oiddaageduidaenigions EEEN 44 LOOMS SMDS isene ia E EE EERE E EEEREN NTENDRE 45 A vertical view over the Software Structure eeeeeeeeceeeeerereeeee 46 3 RATSY Installation and Distribution c cece eecce cece eeeeeeeeenaeeenees 49 3 1 Installing the Binary Distribution 2000 0 eeeee cee ennnneeeeeeeennees 49 3 2 Installing the Source Distribution 2 0 0 0 eee eeeecceeaeteeeeeeeeennees 49 39 Ronnie MARDUK 5 ssa sscaectitciacecwncandac T EE RS 50 SA LACCNSING crnstiiasdocee send cosdecwadsthecedutsavedensteiusdecstandstiaadus enteenieties 50 4A References oo vices ivocnvecsssecsvcesevecesecisectvorslisaievsensocuesvervecuyodenecancaverssvoas 53 RATSY Requirements Analysis Tool Contents e iii
41. ementation for both the patterns In particular any Model can contain observable properties and any Controller is by default an Observer for the Model it is connected to 2 3 Software Structure The software structure of RATSY is strongly affected by the patterns it is based on and by the other software entities it relies on that have been already shown in Figure 44 The main part of RATSY is represented by its core fully based on the MVC amp Observer Infrastructure At the core sides there exist services and resources that are available transversally to the core Figure 45 provides more details about the core and the provided services lt qe Utilities and Services Glade Files lt Ia Tool Stubs Resources Images Threading Control Schemata MVC amp Observer Infrastructure Figure 45 RATSY Software Structure Model Checkers 44 e RATSY Architecture RATSY Requirements Analysis Tool with Synthesis At the leftmost side of Figure 45 are depicted the most important services that are available to models controllers and views These services do not fit well with the MVC and Observer patterns as they do not have any associated view or any user interaction Utilities and Services Contains general utilities globally accessible data etc Tool Stubs Stubs are those entities that isolate RATS Y from the external Model Checkers Stubs export an interface known to RATSY and each model checker has an as
42. ements The input signal for incrementing the value of the counter The input signal for decrementing the value of the counter The value of the counter followed by a decrement of v inc and dec never occur simultaneausly v does not change if no inc and dec commands are issued inc boolean E dec boolean E ys forall M in 6 6 V M amp amp linc amp amp Idec gt next v M g 7 E Check O Consistency BDD Technology v 6 6 S gt Property Assurance Possibilities always forall N in 5 v N gt eventually v N 5 v Partition Threshold Can it be the case the counter changes value CO Cone of Influence Name Trace_4 Dep R1 R2 R3 R4 P1 Figure 15 Counter checking a possibility X H Trace Manager Categories Selected Traces i EEX NEW This is the category of those traces that have been just created gt Trace_1 Category v New 5 traces This is the category of those traces that have been Just created Default empty This ts the default category for traces Out of Date empty Contains the traces whose dependencies might be no longer consistent Traces 28 Show Name category W Trace_1 New E Trace_2 New W Trace_3 New Trace_4 New W Tr
43. en in Property Assurance mode is shown in Figure 4 In the upper part of the body of the window there are the tables for the management of signals and requirements in the middle the are the tabbed tables for the man agement of possibilities and assertions on the left and the control panel for the verification tasks on the right the bottom of the window is occupied by a text box showing the output of the verification activity X 4 RAT Counter x File Edit View Help 3 oe m 9 New Open Traces Assurance Simulation Realizability Signals gt Requirements E a Name Type kna Notes name Kind Property Notes Property Assurance Possibilities Pascuas check Consistency E Name Status Property Notes Sat Technology eoo Technology Solver MiniSAT Y Inc SNF C SEMC Depth 30 Z j Loop All Loops D Checking outcomes Figure 4 Property Assurance main window Adding and modifying elements of a project The activities of adding edit ing and removing items from the sets of signals requirements possibilities and assertions follow the same pattern regardless the class the items belong to The screen shots in Figure 5 and 6 show the windows for creating a new signal a new requirement a new possibility and a new assertion respectively all of which are accessible by clicking on the fi
44. er I Pill M Roveri and S Semprini Manual for property simulation and property assurance tool November 2005 Prosyd Delivarable D1 2 4 5 R Bloem S Galler B Jobstmann N Piterman A Pnueli and M Weiglhofer Specify compile run Hardware form PSL In 6th International Workshop on Compiler Opti mization Meets Compiler Verification 2007 Electronic Notes in Theoretical Computer Science http www entcs org F Buschmann R Meunier H Rohnert P Sommerlad and M Stal Pattern Oriented Software Architecture A System Of Patterns John Wiley amp Sons Ltd West Sussex England 1996 A Cimatti M Roveri and A Tchaltsev Manual for property realizability tool Decem ber 2006 Prosyd Delivarable D1 2 8 R K6nighofer G Hofferek and R Bloem Debugging formal specifications using simple counterstrategies In Formal Methods in Computer Aided Design FMCAD 09 2009 To appear S Minato Zero suppressed BDDs and their applications International Journal on Software Tools for Technology Transfer STTT 3 2 156 170 2001 NUSMV home page http nusmv fbk eu I Pill S Semprini R Cavada M Roveri R Bloem and A Cimatti Formal analysis of hardware requirements In Ellen Sentovich editor Design Automation Conference DAC pages 821 826 ACM 2006 N Piterman A Pnueli and Y Sa ar Synthesis of reactive 1 designs In E A Emer son and K S Namjoshi editors VMCAI volume 3855 of Lecture Notes
45. ers have the form name and may be used in the signal names of the automaton Parameter names may only consist of letters numbers and underscores and must start with a letter or an underscore If you use an automaton with parameters as a requirement an additional field will appear where you can assign values to the parameters Note that you still have to create the RATSY Requirements Analysis Tool RATSY Users Manual e 29 with Synthesis signals that are finally used in your main project including those used to encode the current state of the automaton To facilitate the creation of these signals a refresh button is provided above the signal list which adds all missing signals used by automata The signals created in this way will be marked as automatically generated which means that if their names change or they become obsolete for example because the requirement using them was deleted you can easily update them by clicking refresh again You may edit an automatic signal as well for example to change its type but in this case it loses its automatic status and has to be maintained manually 1 5 Simulating and Debugging Specifications using Games The game part of RATSY provides three main features It allows you 1 to play a normal game in order to test the specified system 2 to play a countergame in order to understand why a certain specification is unrealizable and 3 to specify desired behavior if undesired behavior was ob
46. gure 43 The state of the play in an automaton RATSY Requirements Analysis Tool RATSY Users Manual e 39 with Synthesis 40 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis 2 RATSY Architecture In the following the design and implementation of RATSY will be discussed The general information about RATS Y implementation and run time environment will be described in Section 2 1 Section 2 2 explains architectural patterns used dur ing RATSY development The hierarchy of the RATSY software is described in Section 2 3 2 1 Architecture and Implementation Notes RATSY is a stand alone multi platform application that runs in one process Even if multi threading is used to run external verification engines the GUI part fits into a single main thread RATSY has been fully developed with the Python object oriented programming language and the GUI part relies on the PyGTK graphical toolkit to draw itself to the screen and to handle the interaction with the user The coding followed a few standards de facto Classes methods and functions names follow PyGTK s convention see http www pygtk org that derives from the GTK s one see http www gtk org Style and indentation are strictly Python compliant Packages and filenames are java style but slightly less restric tive e g a file foo_and_foo py contains definition of class FooAndFoo but may contain the definitions of other classes if convenient
47. gy and attempts to obtain a countertrace from it Our heuristic is able to find such a countertrace This countertrace is used in the countergame as depicted in Figure 42 It sets startup_failed 1 and r0 This example is included in the RATSY distribution examples demo DemoGame2 rat The corresponding project file is RATSY Requirements Analysis Tool RATSY Users Manual e 37 with Synthesis 1 forever Due to our design intent error must be raised Due to sys tran 1 no grant on error no grant can be given Additionally r0 1 forever so the guarantee sys fair 0 cannot be fulfilled This explanation is also given by the tool in the Game Log of Figure 42 Game X Gane Log x opas We are now in step 3 already selected input values for this step A S SEDA SAPA SELES SIERA SER ro error setto 1 rl We are now in step 4 already selected input values for this step startup falled error set to 1 We are now in step 5 already selected input values for this step ix error set to 1 ix Step 5 is now part of the infinite loop E R You lose g Why I can tell you state in graph All safety constraints are enforced during the play ____________ For the fairness constraints the situation is as following Outputs fairness_assumption 0 is fulfilled in the step s 5 Step1 Step2 Step3 Step4 Step5 go fairness_guarantee 0 is not fulfilled in any step of the loop a fairness_guarantee 1 is fulfilled in the step
48. he environment to find prob lematic inputs i e inputs for which no behavior of the system can fulfill the spec ification The inputs suggested by the counterstrategy depend on the outputs pre viously chosen by the user On the other hand a countertrace is a fixed trace 34 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis of inputs for which no behavior of the system can fulfill the specification It is independent of the moves of the system and thus easier to understand RATSY heuristically searches for a countertrace If it could find one this countertrace is used instead of the counterstrategy in the countergame The complete countertrace is shown right from the beginning of the play so you know in advance how the environment will behave This makes it easier for you to localize the problem in the specification Summarizing Graph A graph is computed that summarizes all plays that are possible when the environment adheres to the counterstrategy or the countertrace Its vertices correspond to states in the game edges correspond to state transitions which are possible in the game This graph can be seen as a cheat sheet for the interactive game It allows you to see how the environment will react to your outputs Thus you may discard some choices a priori This reduces the number of plays necessary to understand the cause of unrealizability The graph is written in two version into the files game_data graph
49. he synthesis fea ture of RATSY the game part requires the specification to be in the Generalized Reactivity format i e at least one assumption and at least one guarantee must be a fairness liveness constraint Otherwise an according error message is printed when trying to start a game 30 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis How to play a Game Figure 37 shows the Game window in action Initially the trace views labeled with Game X Game Log s 5 Step1 Step2 Step3 Jiii Dumping the specification into tmp xml a ep ee e pail hready Starting Marduk with the file l hbusreqo Checking for realizability may take some time hlocko The spec is realizable g l e there is a system that implements the specification will now synthesize hbusreq1 such a system hlock1 Synthesizing the strategy may take some time a Starting the game _ Fix value to False b Outputs With the interactive game cou can test the system synthesized The game is A Fix value to True tep3 isi hinasterd played in the following way You are in he role of the environment andi aminthe w Set to Do not care maak Show Results v Show Operations wv Show Help Remove time step from loop start a decide v Start Stop Next Step Clear Prev Step Done Export Show Subviews Hide Subviews e Play Game Options for unrealizable specs v Sat Check v Minimize v Compute Graph Specify De
50. heck of the analysis reassures our preliminary conclusions To gain a more in teresting trace we request a request to eventually happen as illustrated in Figure 23 We keep the analysis window opened and ask for a new witness by pressing the corresponding button in the main window We are presented with the trace illustrated in Figure 24 As we are satisfied with the trace and want a request to happen for future examples we change our property RATSY Requirements Analysis Tool with Synthesis 18 e RATSY Users Manual 5 CAMINE x Formula coverage gt request features Signal Formula o f fc o fi c fo 1 c FED G 1 F 0 G 0 Y Gl r gt F a 010 r gt F a r V F a a Figure 23 Ask for a request on signal r to G r gt F a amp amp F r By asking for a new witness we want to recheck this change Please note that the requests are reset for every trace so you might not include a forgotten request forever resulting in the miss of interesting behaviors during property exploration X SE o File Edit View Help Open Traces Assurance Simulation Realizability Property Signals Requirements Possibilities Assertions G lr gt Fa Property Simulation Signals step1 step2 steps Step4 Step5 2 r a Evaluation step1 step2 steps Step4 StepS 7 Gin gt F r gt Fla r V F a a
51. ironment Now we can check that the system ex hibits desired behaviors i e that it is possible that something happens even if not mandatory For example we may want to check that it is actually the case that the value of the counter may change this means looking for a scenario in which the system evolves reacting to the stimuli of the environment in such a way to modify the initial value of the counter This check can be performed by the possibility P1 shown in Figure 15 The possibility is signaled as passed in the Possibilities table and a trace cor responding to a witness of the desired system behavior is shown the trace exhibits a five step loop in which initially v is 1 and two consecutive inc operations are issued the value of v changes accordingly and then two dec operations are issued making the value of v going back to 1 in the fifth step The result of a work session is a specification a set of possibilities a set of as sertions and a set of traces corresponding to the results of the checks performed Figure 16 shows the trace manager window with the traces generated during this session actually other traces are shown that we do not described but that have been generated within this section 12 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis Xa RAT DemoPropAssurance 0X File Edit View Help BoQ m New Open Save Traces cs Simulation Realizability 20060 gt Requir
52. is Way points can also be deleted by selecting them left click and using the Delete button on the right hand side Next add loop edges to both s0 and s1 Doing so is straight forward Just click New Edge and then click twice on the state you want to have a loop edge After you have created all the states and edges we are going to specify the tran sition condition for the edges The idea is that state s0 is the state in which there are no outstanding requests Thus it is an accepting state and should be visited infinitely often On the other hand s1 is the state in which there is a request which has not yet been acknowledged So the transition from s0 to s1 should be taken whenever req 1 and ack 0 Double click the edge to edit its properties cf Fig 35 In the Minterm field enter 10 meaning req 1 and ack 0 If there is no z aax Name i 0 Minterms 11 caca ok Figure 35 Specify the transition condition for an edge request req 0 we don t care about the value of ack and stay in s0 Also if a request is immediately answered req 1 ack 1 we stay in s0 These two cases correspond to the minterms 0 and 11 Enter them for the loop edge on s0 one minterm per line For the state s1 we want to stay there as long as we do not an swer the outstanding request Thus set the minterm for the loop edge to 0 You will notice that the edge from s1 to s0 is automatically updated from true to ack beca
53. ither a witness or a counter example In RATSY there exist several view over a trace as they can occur within the main application window and within the Trace Manager window In general a trace can be shown as a graphical waveform with some associated information like the category it belongs to the number of steps the loop information etc Property This entity represent a single property like a requirement or a possibil ity The model contains information about the property like the name and formula The view is shown when the user wants to create or edit a prop erty There exist a dependency between a property and those traces there were generated from it Whenever a property s formula is changed the cor responding traces will be invalidated More information about RATS Y implementation details can be obtain in 2 48 e RATSY Architecture RATSY Requirements Analysis Tool with Synthesis 3 RATSY Installation and Dis tribution This section gives information on installation and distribution related issues RATS Y can be downloaded in the form of binaries for 32 bit and 64 bit Linux systems and also as a source tree 3 1 Installing the Binary Distribution To start RATSY from the binary distribution simply extract the downloaded archive into any directory and start the script ratsy ratsy For more convenience you can add the ratsy folder to your PATH environment variable The archive contains binaries of all external t
54. ks related to these four methodologies All the examples in the following sections are written in the Verilog flavor of PSL as from 12 the language supported by the verification engines VIS and NUSMV Some of the screenshots in this manual especially in the sections about Property Assurance and Property Simulation were taken from a previous version of the tool RAT Thus they might look slightly different than what you will see in the current version RATSY This should however not affect understanding of the respective sections 1 1 Running RATSY RATSY can be executed from the command line by the following command ratsy Launches the python interpreter to execute the Command RATSY program ratsy h help v version f lt FILE rat gt project lt FILE rat gt Command Options h Prints the command usage v Prints the program version f lt FILE rat gt Loads the given project file Figure 1 shows the start up screen shot of RATSY when the tool is launched with out any project as argument The unit of interaction with RATSY is the project i e a collection of formal pro perties and results of verification checks The relevance of the role of a project as an object with a state that can be saved and reloaded is clear as far as Prop erty Assurance and Property Realizability are regarded the user that builds formal specifications and inspects their quality must have the possibility to work in dif
55. l informal design intent was that the output signal error has to be set indefinitely if startup_failed is always set after the first time step This behavior cannot be observed in Figure 39 You can now switch into the Specify Design Intent mode in order to use the simulation trace as starting point for the definition of the desired behavior This example is included in the RATSY distribution The corresponding project file is examples demo DemoGamel rat 36 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis Automata x Name Notes design_intentO Created automatically from a simulation run Game Inputs Step1 Step2 ro rl startup_failed A v Outputs Step1 Step2 90 i A v gl error Figure 40 The specified design intent Figure 40 shows the result of the specification of the desired behavior When startup_failed 1 right after the initial state until infinity then so must be the output signal error Click the Done button and an automaton is created automatically which accepts only the desired behavior Add the automaton to the specification and obtain the specification depicted in Figure 41 Signals X Requirements amp Name venvinit A t OxX Name Kind Notes Kind Automaton Type Property rO 0 amp amp r1 0 amp amp startup_failed 0 b INE re er y entity 0 r1 boolean E resource request by entity 1 vsysinit G g0 0 amp amp g1 0
56. lly create edit the automaton In the main automaton editor window click the buttons New State and then click on an empty spot in the editor pane to add a state to the automaton Double click the state to edit its properties Fig 34 You can specify a name for the state whether or not it is the initial state of the automaton and whether or not this state is one of the accepting states Name the state s0 and make it initial and accepting Create a second state which should not be accepting and label it s1 You will notice that the new states have a dangling edge labeled true Dangling edges lead to an im 4This example is included in the RATSY distribution The corresponding project file is examples demo DemoAutomaton rat 26 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis Ped arbiter Hog Create a new automaton Name Automaton Generate dead state formula J Edit amp if cance Sok Figure 33 Create a new automaton P anx J Final Z Initial Q cancel ok Figure 34 Edit the properties of a state in the automaton plicit non accepting dead state which has a self loop labeled true For reasons of clarity this dead state is not drawn explicitly The editor keeps the automaton deterministic and complete at all times Since we have not specified any transi tions yet all transitions hence the label true lead to the dea
57. n the source distribution of RATSY For convenience the build script of RATS Y automatically downloads the VIS sources however Note that the license for RATS Y VIS sources and NUSMYV sources allows for commercial use currently the use of VIS and NUSMV takes place in commercial settings nttps swig svn sourceforge net svnroot swig trunk Tools pyname_patch py 50 e RATSY Installation and Distribution RATSY Requirements Analysis Tool with Synthesis The development of the first version of this tool RAT has been supported in part by the European Union under contract 507219 PROSYD The current version RATSY has been supported by the European Union under contract 217069 CO CONUT and 248613 DIAMOND as well as by the Provincia Autonoma di Trento project EMTELOS lOnttp www prosyd org http www coconut project eu Http www fp7 diamond eu RATSY Requirements Analysis Tool RATSY Installation and Distribution e 51 with Synthesis 52 e RATSY Installation and Distribution RATSY Requirements Analysis Tool with Synthesis 4 1 2 3 m 5 6 7 8 9 10 11 12 13 References R Bloem R Cavada A Cimatti I Pill M Roveri S Semprini and A Tchaltsev RAT A tool for formal analysis of requirements In Demo Session of the 17 European Conference on Artificial Intelligence Riva del Garda Italy 2006 R Bloem R Cavada C Eisn
58. n of Property Simulation Assurance and Realizability into RATS Y rather than simply juxtaposing them it is possible to shift between these three kinds of projects at any time and to load properties for example from Property Assurance into Property Simulation or Property Realizability A project hence sums up all the history of a design development process from the initial ex plorations of properties prototypes to the definition of a set of requirements from the inspection of requirements adherence to the intended meaning to the possi 2 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis X BRR x Other optional project information Project File Counter Project Notes The specification of a counter modulo 5 R Cancel lt Back amp Finish Figure 3 RATS Y New project wizard project data ble use of simulation to perform a fine grained inspection of properties coming from Property Assurance and to checking the interplay between controlled and uncontrolled signals and their requirements with Realizability Once a project has been created the user can proceed as described in Sections 1 2 1 3 and 1 4 1 2 Property Assurance in RATSY RATSY enacts the Property Assurance Methodology see 2 Section 2 2 by sup porting the users in Property Assurance related tasks RATSY provides a proper framework for managing set of propertie
59. ncentrate on fulfilling this fairness constraint only The environment can change this index a finite number of times The maximal number of changes of jx is contained in the waveform jx changes All these values are addressed to advanced users they can also be ignored RATSY Requirements Analysis Tool RATSY Users Manual e 35 with Synthesis Example This section illustrates on a concrete example how the game features can be used We will use the specification depicted in Figure 38 It defines a simple arbiter for some resource shared by two entities With the inputs r0 and r1 access to the resource can be requested by entity 0 and entity 1 respectively With the out puts g0 and g1 the resource is granted to the entities The output error signals an error Forget about startup_failed for a moment All signals are initialized to 0 env init and sys init There is a guarantee that enforces that the re source is not granted to both entities at the same time sys tran 0 There is a guarantee that ensures that no grant is given in case of an error sys tran 1 Finally there are guarantees that state that every request must be granted eventu ally sys fair 0 and sys fair 1 The assumption env fair is added so that NUSMV identifies the specification as a Generalized Reactivity 1 specification and not as a B chi game specification Remember that games can only be played on Generalized Reactivity 1 specifications Signals X Req
60. ncrementing the value WIR2 G V M amp amp dec gt next v M 1 followed by of the counter a decrement of v The input signal for Z R3 A never inc amp amp dec inc and dec never occur dec boolean E decrementing the simultaneausly value of the counter always forall M in 6 6 v does not change if no v 6 6 S The value of the counter i V M amp amp linc amp amp Idec gt inc and dec commands next v M are issued y gi BE sibilitie Assertions pas 3 Check CO Consistency 206 Sat Technology BDD Technology always forall M in 5 5 v does not change if Partition Threshold v al v M gt v M until inc dec there are no inc and dec Lod L Cane nf influence hi Z Checking outcomes done bed Flattening the generated tableau done Creating LTL tableau variables specification always forall M in 6 5 v M amp inc gt next v M 1 amp always forall M in 5 6 v M amp de S Clear There are no traces currently available Quitting the BMC package Done gt Output Figure 14 Counter fixing the specification the Sift dynamic reordering method In this case no trace is shown because no counterexamples has been found Once the check for Al is passed we gained more confidence on how the counter reacts to the stimuli of the env
61. ntroller the data processing to the Model and the result presentation to the View In RATSY this pattern is implemented in the MVC and Observer Infrastructure This implementation wanted to be different from the traditional one as it is spe cific for the underlying graphical toolkit PyGTK and language Python to exploit their peculiarities and features In particular a part of the traditional View s fea tures have been moved to the Controller and the model has been made not aware of the existence of any Controller or View In combination with the Observer pattern see next section this allows for a real separation of the application logic from the presentation layer Model Contains the logic of the program intended as data and data manipulation routines Models can communicate with other models especially with mod els that they contain but do not know the other parts of the MVC pattern namely the Controller and the View This limitation guarantees the insulation between the application logic and presentation View Contains the presentation layer The View constituted by a set of graphical widgets organized as a forest typically a single tree A single widget is one atomic GUI element like a button a text label a window etc Often widgets are containers for other widgets hence widgets are organized in trees where vertices represents the containment relations As for the models views do not know the models they are connecte
62. occur 10 e RATSY Users Manual never inc amp amp dec simultaneausly t 4 Property Assurance Assertions 208 Possibilities a Check Sat Technology EDD Technology iv Consistency A Name status propery Notes Inc SBMC SNF Solver MiniSAT Y Tal w Depth 30 7 Loop All Loops lv Checking outcomes Destroying a SAT solver instance MiniSat Done Quitting the BMC package Figure 12 Counter initial specification inc the signal that models the issuing of increment operations dec the signal that models the issuing of decrement operations v the signal integer valued that models the value of the counter this signals are shown in the Signals table together with their type and notes The Requirements table collects three requirements that constitute an initial spec ification of the functional behavior of the counter and of the assumptions on the environment R1 prescribes that any increment operation is immediately followed by a unit increment in the value of the counter R2 prescribes that any decrement operation is immediately followed by a unit decrement in the value of the counter R3 states that increment and decrement operations must not occur simultane ously this is a constraint on the environment On
63. ools such as the model checkers VIS and NUSMV You do not need to download and install them separately The one exception is the tool LILY which is needed to perform realizability checks on full LTL specifications not only on specifications given in Generalized Re activity 1 format If you do not need this feature then you do not have to install LILY If you do simply download Lity extract the archive patch it with NuSMV game nugat contrib Lily 1 0 2 patch and include it into your PATH and PERLSLIB environment variables 3 2 Installing the Source Distribution To build RATSY and all the external tools such as the model checkers VIS and NUSMV from source simply extract the downloaded source archive into any di rectory and execute the build sh script in the top level directory Follow the instructions of this script As for the binary distribution if you need support for full LTL realizability checking you have to install LILY see Section 3 1 When the build process has finished the script ratsy ratsy starts up RATSY Known issues 8http www iaik tugraz at content research design_verification lily RATSY Requirements Analysis Tool RATSY Installation and Distribution e 49 with Synthesis e The NuSMV wrapper does not compile with Swig Version 1 3 39 or above installed The reason is that Swig changed interface names see http www swig org Release CHANGES at date 2008 12 04 without backward compatibility As a workaroun
64. pendent and the internal sub part Tool Stubs insulates RATS Y even from the model checkers 2 2 Architectural Patterns RATSY has a pretty complex structure as it currently fits in six packages about 68 modules and 21400 lines of Python code including comments excluding blank 42 e RATSY Architecture RATSY Requirements Analysis Tool with Synthesis lines RATSY is characterized by strongly interconnected features and by the need of horizontal communication among independent parts Furthermore it pro vides many different independent views over the same objects and those views are often potentially editable by the user Whenever one of those view is changed by the user or by RATSY itself all the other should react accordingly To reduce the structural complexity to keep a clean design and to minimize the development and maintenance costs two architectural patterns were considered The Model View Controller MVC and the Observer patterns see 4 The Model View Controller pattern MVC is an architectural pattern that forces the designer to break up the application being designed among three main parts a Model a View and Controller The traditional implementation of this pattern reflects the normal data flow of non GUI applications data input data processing and result presentation Historically the MVC pattern is an attempt to map this natural data flow to the GUI design In fact it associates the data input to the Co
65. perty Simulation mode this can be accomplished by selecting the desired items and clicking on the last one among the four buttons on the top right corner of the proper table or by selecting the voice Load into Simulation from the pop up menu accessible by right clicking on the selected items The logical conjunction of the selected items is copied in the Property text box in the Property Simulation mode See Section 1 3 Verification The verification tabbed panel on the middle right of the window provides the user with control on the execution of the verification engine used to perform Property Assurance related checks The two tabs shown in Figure 7 al low to chose among SAT based BMC techniques or BDD based MC techniques and to set the respective options As far as SAT based BMC is regarded it is pos sible to choose which SAT solver to use whether incremental techniques should be used the depth of the BMC problem generated and the value for the loop back With regard to BDD based MC the user can define the partition method whether using Cone of Influence techniques and which kind of dynamic reordering should be used if any For more details on the meaning of these options the user can refer to the user manual of NUSMV 8 6 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis Check Consistency Check Consistency Sat Technology BDD Technology Sat Technology BDD Technology Solver MinisAT v
66. re 38 The specification used for Game dem0 ceeeeeeee eee 36 Figure 39 A possible simulation run cece eee eeeeneeeeeeeeeaeeeeeeeeeea 36 Figure 40 The specified design intent 0 0 0 cee ceeeeeeeeceeeeeeeeeeeeeeea 37 Figure 41 The new specification containing the desired behavior 37 Figure 42 The countergame containing the countertrace 4 38 Figure 43 The state of the play in an automaton cceeeeeeeeee eee 39 Figure 44 RATSY Software parts and collocation eee 42 Figure 45 RATSY Software Structure ec cceeeeeeeeeeeneeeeeeeeeee 44 Figure 46 RATSY Hierarchy of main software entities 04 46 RATSY Requirements Analysis Tool Table of Figures e v with Synthesis List of Tables vi e List of Tables RATSY Requirements Analysis Tool with Synthesis RATSY Requirements Analysis Tool List of Tables e vii with Synthesis viii e List of Tables RATSY Requirements Analysis Tool with Synthesis 1 RATSY Users Manual The tool RATSY fulfills the need for a proper technological support to formal methods in the setting of requirements analysis and synthesis by providing its users with the integration of four sets of functionalities Property Simulation Property Assurance Property Realizability and Synthesis and Property Debugging using Games In this section we show how to interact with RATSY in order to accom plish the tas
67. re shown on the right part of the window grouped under the name of the category they belong to In the left 8 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis bottom corner of the window there is the list of the names of the traces contained in the selected categories by selecting or de selecting names it is possible to show or hide traces in the right part As shown each trace is visualized together with its complete data that comprise a brief description the notes entered by the user the list of dependences and the history when the trace was generated etc Categories and traces tables on the left part of the window allow the users to edit delete or add items in Figure 10 and Figure 11 the editing dialog for categories and traces are shown X M o Add a new Category Name New Description This is a category of those traces that have been just created Cancel 2 OK Figure 10 Editing a category X Da PALE Edit Trace Information General _ Name Trace_6 Category New v Notes Other information Description This trace contains 3 steps and has one loop at step 2 Dependencies ro rl poss0 Originating formula CCalways a b next c amp eventually Ca amp amp b amp amp Creation information Created by NuSMV on Thu Dec 14 16 59 46 2006 Checking command was check_pslspec b k 30 1 History 00 Added
68. ring the tree structure and the coverage information can be of great help in exploring the behavior of a property Considering the example of a property requiring an request to be acknowledged the coverage information may show that there is no request happening columns labeled 1 show zero values for request for a vacuous trace So by setting the request to be eventually true you can ask for a more interesting trace for example When a part of the property doesn t evaluate to a specific value at any time you may ask for an illustration of what happens if it does by seating the corresponding request X n EIR ueo ee x Formula coverage gt request features FES EE Fa Ee aL 7 G r gt F a 0020 0S0 r gt F a r F a Figure 18 Property Simulation Evaluation Analysis Window 16 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis An example This section illustrates RATS Y Property Simulation functionality with a simple example For this example scenario we will consider the informal property that a request should be eventually acknowledged First we have to start a new project This is done by calling rat and clicking the New button at the top of the window As for this example we decide to do Prop erty Simulation only we can skip the step of entering project details at this stage Property Simulation extracts the information it needs for its computations direc
69. roperty Assurance Real izability Synthesis and the Games Requirements This entity contains the set of requirements used by Property As surance Realizability Synthesis and the Games Automata This entity contains the set of automata Automata can be instantiated to Requirements Property Assurance This is the entity for Property Assurance Its view is shown when the Property Assurance feature is selected at the application level Property Simulation This is the entity for Property Simulation Its view is shown when the Property Simulation feature is selected at the application level Property Realizability amp Synthesis This is the entity for Property Realizability amp Synthesis Its view is shown when the Property Realizability amp Synthesis feature is selected at the application level Games This is the entity for playing games Its view is shown when the Game feature is selected at application level This entity is quite interweaved with MARDUK and hence accesses MARDUK directly and not via a stub Traces Manager This entity handles the set of traces that have been generated in the project Also this entity organizes the set of traces within a set of categories that traces belong to RATSY Requirements Analysis Tool RATSY Architecture e 47 with Synthesis Assurance NUSMV Stub The Property Assurance NUSMV stub handles the in teraction of RATSY with the NUSMV model checker when Property As surance is run This en
70. roperty into the en try widget of the Property Simulation main window and press the Witness button to ask for an example trace fulfilling and illustrating the property We re presented with the trace illustrated in Figure 21 X FRG ae ARK File Edit View Help Open Traces Assurance Simulation Realizability Property Signals Requirements Possibilities Assertions Gir gt F a Name Type Kind Notes Property Simulation Sa mag r a ka Evaluation steps Step2 Step3 F Ga gt F a Y r gt F a r Y Fla a ic t gt Witness Counterexample Status Result Witness Analysis Figure 21 Witness for property G r gt F a The trace is vacuous because there is no request but actually there are acknowl edges We see that the property does neither need a request to happen nor that there is a request for an acknowledge to occur Although the example is very sim ple and we can obtain that information by judging and interpreting the waveforms we now press the analysis button to show the coverage information illustrated by Figure 22 o X CEARA Formula coverage gt request features sionaiyrormua Jo fa feo ife pile fen een rao eeo 7 G r gt F a 010020030 r gt Fla r Y F a a Figure 22 Analysis of trace for property G r gt F a A c
71. rst one among the buttons on the top right of the table of the proper class 4 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis Note that in Property Realizability signals are distinguished of being System or Environment Similarly requirements are distinguished of being Assumption or Guarantee For Property Assurance and Property Simulation these distinctions are of no importance and therefore ignored X N o x Create a new signal f Name inc Kind Environment O System Type Boolean O Other gt Editor Notes The input signal for incrementing the value of the counter 3 Cancel 2 ok yar o gt Create a new requirement Name R1 Property always forall M in 6 5 v M amp amp inc gt next v M 1 Kind Guarantee Assumption Notes leach inc is immediately followed by lan increment of v Figure 5 Creating signals requirements Once an item is created it is shown in the table of its class and it is possible to modify or to delete it by clicking on the proper button on the table of the class of the item A window similar to the one used for creation is used for editing and a warning window will ask for the user s confirmation before deleting an item Mul tiple selection is allowed Ctrl keyboard button pressed when left clicking with the mouse on the desired items and hence is possible
72. s a user friendly interface towards ver ification engines and a proper framework for managing the results of Property Assurance proof obligations In this section we describe how to interact with the tool by following a typical use case which encompasses the following steps e editing of a project editing of signals editing of requirements editing of possibilities editing of assertions e verification activation of the checks management of traces In the setting of Property Assurance Projects are the entities that correspond to the ensemble of a specification together with the results obtained by the connected proof obligations The building blocks of a specification in the Property Assurance Methodology are requirements possibilities and assertion all of which are proper ties formally expressed on a set of atomic symbols called signals Following the RATSY Requirements Analysis Tool RATSY Users Manual e 3 with Synthesis methodology given a specification some proof obligation need to be discharged in 2 Section 2 2 it has been shown how these proof obligations can be mapped onto SAT technology the tool provides an interface towards this technology and communicates the results of the performed verification checks by means of ex tended waveforms called traces that show the evolution of the values of signals in possible models of the system under specification The Main Window RATSY main window wh
73. served during a play In the normal game you are in the role of the environment while the tool is in the role of the system In every time step you first choose values for the inputs Then the system responds with outputs that conform to the specification In order to find such outputs a winning strategy for the system is synthesized In the countergame you are in the role of the system while the tool is in the role of the environment In every time step the tool first provides input values You are then asked to choose the values of the outputs in such a way that the specification is fulfilled You win if you manage to fulfill the specification You lose otherwise The tool uses a counterstrategy to find problematic inputs i e inputs for which no behavior of the system can fulfill the specification Hence you will lose for sure However while losing you will understand where the specification is too restrictive to be realizable This knowledge can then be used to correct the specifi cation in order to obtain a realizable specification More information on debugging unrealizable specifications with countergames can be found in 6 As within Property Realizability signals are distinguished of being under the con trol of the system or the environment Furthermore requirements can be assump tions or guarantees The specification requires the system to fulfill all guarantees if all assumptions are fulfilled by the environment Similar to t
74. session in batch mode A vertical view over the Software Structure The RATSY software structure has been split horizontally by using the MVC and Observer Infrastructure There exists also a vertical splitting that breaks the soft ware structure up through a hierarchy of software entities Application Property Property Zotomala Synthesis Assurance Possibilities Propert Traces Property Requirements Ope ry Signals Realizability Simulation Manager Realizability Assurance NuSMV Stub NuSMV Stub sigeuy Figure 46 RATSY Hierarchy of main software entities Figure 46 depicts the hierarchy of the main software entities that occur within RATSY Each of the boxes represents a software entity and each vertex of the hierarchy tree is a containment relation where cardinality is not expressed That means for example that an Application contains one or more software entities to represent a Project and the Options of the Application The way each software entity is implemented depends on the entity s role Those entities that need to be shown will follow the MVC pattern and will be mapped 46 e RATSY Architecture RATSY Requirements Analysis Tool with Synthesis down to three object oriented classes or to a triple of a limited set of classes to as sociate to each entity a Model a View and a Controller For example the entity ap plication s Options has a model to hold the options and a couple
75. sign Intent Figure 37 The Game window in RATSY Inputs and Outputs are empty The button Start starts the game First the tool checks the specification for realizability If it is realizable a normal game is started otherwise a countergame is started In either case the current time step of the game is marked with red letters You are only allowed to modify signal values in the current time step Signal values can be modified by right clicking onto the according position in the trace A pop up menu appears that allows to set the value to 0 1 or don t care see Figure 37 In the normal game you are only allowed to modify input signals In the countergame you can only modify the output signals Different waveform colors are used to mark different origins of signal values e Black is used if the signal value is the only possibility fulfilling the safety requirements e Red is used for user selections e Blue is used if the signal value is a consequence of some user selection for other signals e Green is used if the signal value was chosen completely arbitrarily During the play the tool enforces that all safety requirements are met When your choice violates some safety requirement an error message is printed After setting all signals to their desired values in the current time step click Next Step and the next time step can be edited By clicking Clear all user selections for the current time step are
76. sociated stub The result is that RATSY can call a model checker careless of the specific Model Checker it is actually calling Threading Control Provides fine grained portable control over threads This ser vice is used for example in stubs invocation for running the model checkers in background for controlling the associated process and for capturing its output At the rightmost side of Figure 45 are depicted those resources that are exclusively used by the RATSY Views Noticeable resources are Glade Files As already mentioned a Views is a forest of widgets The widgets can be build and connected each other by hand or by using programming tools like glade see http glade gnome org This tool can be used to visually design a forest of widgets representing the view s widgets With very few limitations this tool can be used then to set the properties of all widgets and to associate action to be carried out when a certain events oc cur signals For example a widget like a button can be associated with a function name to be called when clicked The result of this creation and set ting process is a glade file that can be loaded at runtime by the MVC and Observer Infrastructure that provides the needed support for Views creation based on glade files and to connect the associated Controllers that provide the implementation of signals actions Images Contains icons and other images to be shown by the views Tools Stubs As alrea
77. stem Libraries Those depend on the specific architecture implemented on the host computer Currently RATS Y has been tested under GNU Linux with a 2 4 and 2 6 kernel GTK Toolkit GTK is a set of libraries that provide a pretty platform independent support for drawing and handling graphical widgets like windows buttons text entries fonts etc See http www gtk org for further information about GTK and its components Python Library This is a general multi platform runtime environment provided by the Python environment It provides a large set of features and data structures to be used from any Python based application It also provides a portable abstraction layer over the underlying Operating System making the application platform independent See http www python org for further information NUSMV and VIS_ These are the Model Checkers RATSY is currently based on MARDUK is a command line Python program for synthesis and specification de bugging PyGTK Bindings This is a Python binding that allows Python programs to use the GTK Toolkit See at http www pygtk org for further information MVC amp Observer Infrastructure This is a Python package that helps to design and develop GUI applications It implements the Model View Controller and the Observer patterns developed specifically for PyGTK RATSY Application This is the set of Python packages that implement the RATS Y application The underlying layers make RATSY platform inde
78. tart Changes of the specification that are made during a play do not affect the play One has to click Stop followed by Start to start a new game using the modified specification Game traces can be exported by clicking the button Export You can choose between three formats jpeg png and vcd Value Change Dump Exporting the game traces as jpeg or png improves over a simple screenshot in that no part of the trace is hidden due to scroll bars Game traces exported as vcd can be opened by most waveform viewers However the colors in the trace as well as the position of the infinite loop are lost when exporting traces as vcd This is due to a lack of support of such elements in the Value Change Dump format Note that there is currently no way to save the current state of a play In particular exported game traces cannot be loaded again to continue a play There are two sub windows related to the Game window the Game Log window and the Automata window Both can be shown or hidden with the buttons Show Subviews and Hide Subviews respectively These sub windows are described in the next sections The Game Log Window The Game Log window is also shown in Figure 37 It contains three types of log messages e Results Written in red they contain the main results obtained by the tool during the play e Operations Such messages show what the tool is currently doing They are written in black e Help Messages These messages guide you thro
79. te that a summary of the information related to the trace is provided close to the trace itself By examining the trace we notice that the counterexample shown has an initial step in which the value of the counter is 2 and no operation is issued and a second step in which the value of the counter is changed to 4 Note that the last state is actually the first and only one of an infinite loop as signaled by the little black arrow close to the name of the step in the header of the trace A review of the requirements reveals that actually nothing is said about the evolution of signal v when no operation is issued and this leads us to the definition of a new requirements that fills this hole R4 prescribes that if no operation is issued the value of the counter remains un changed Figure 14 illustrates the new state of the specification and shows that if R4 is added the check for Al passes as signaled by the green bullet in the Assertions table Note that in this case the check has been performed using BDD technology with RATSY Requirements Analysis Tool RATSY Users Manual e 11 with Synthesis X u RAT DemoPropAssurance OXx File Edit View Help New Open Save Traces Assurance Simulation Realizability Signals 2 8 Requirements z i 1 Name Type kna Notes A Name Kind Property Notes had The input signal for always forall M in 5 6 each dec is immediately inc booleanE i
80. terminate abnormally Unfortunately the synthesis process can not give information about which of the requirements is malformed The error message in the Checking Outcomes window will look like this ERROR Encountered an exception Error could not parse the input file If you click the Check Realizability button without changing your specification the real izability check will report in more detail which of your requirements is malformed These information will be displayed in the Checking Outcomes window The Automaton Editor Specifications for reactive systems are often easily expressible as a set of deter ministic and complete Biichi word automata where the edges correspond to safety constraints and the accepting states correspond to fairness liveness constraints RATSY provides a graphical tool to create and edit such automata The automata are automatically converted into PSL formulas which can then be used as require ments The following example illustrates the use of the automaton editor Think of a very simple arbiter with just one request line req and one acknowledge line ack We want to model a property that captures the fact that every request should eventually be acknowledged We will do so by means of a simple Biichi automaton with 2 states First click the plus sign above the automata list to add a new automaton In the dialog window that opens Fig 33 specify a name for this automaton Then click the Edit button to actua
81. tities has no associated View and Controller and it is implemented by a single class This class is the specialization of a more generic classes hierarchy that provides support for implementing specific tool stubs Realizability NUSMV Stub The Property Realizability NUSMV stub handles the interaction of RATSY with the enhanced version of NUSMV 5 when Property Realizability is run This entities has no associated View and Con troller and it is implemented by a single class Similarly to the Property Assurance NUSMV Stub already available in RATSY this class is the spe cialization of a more generic classes hierarchy that provides support for im plementing specific tool stubs MARDUK The MARDUK tool handles synthesis as well as strategy computation for the Game features MARDUK Stub Like the NUSMV Stubs entities but specific for MARDUK Possibilities Contained within the Property Assurance entity this entity repre sents the set of possibilities for Property Assurance Assertions Contained within the Property Assurance entity this entity represents the set of assertions for Property Assurance Signal This entity represent a single signal The model contains information about the signal like the name and type information The view is shown when the user wants to create or edit a signal Vis Stub Like the NUSMV Stubs entities but specific for the VIS model checker Trace A trace is the result of model checking and can represent e
82. tly from the property itself With a click on the finish button Figure 19 we are pre sented with the main window of Property Simulation Figure 20 Please note that if you would like to perform Property Simulation in an existing requirements engineering project for a device under construction you can switch to Property Simulation by clicking the control button at the top right of the main window X BEE o Specify the initial project type OPr O Realizability Property Simulation allows for Note It will be possible to switch among the project types at any time 3 Cancel P Forward Finish Figure 19 Create a project for Property Simulation 4 SE o x File Edit View Help Open Traces Assurance Simulation Realizability Property Signals Requirements Possibilities Assertions Property Simulation Signals Evaluation is lt gt Witness Counterexample Status Result Initialized Analysis Figure 20 Property Simulation Start Window Our first guess on PSL syntax for our informal property is G r gt F a G Glob ally is the short form of the PSL operator always and F Eventually Finally RATSY Requirements Analysis Tool RATSY Users Manual e 17 with Synthesis 7 is the short form of the eventually operator We enter that p
83. to category New lt gt Cancel 2 OK Figure 11 Editing a trace An Example In this section we work out a simple but meaningful example that covers the most relevant Property Assurance features of RATSY and link together in a cohesive view the usage information given in the previous section The example we are going to tackle is the specification of a bounded counter an instantiation of what described in 2 Section 2 2 a first naiv specification could be the one shown in Figure 12 The specification is based on the following signals RATSY Requirements Analysis Tool RATSY Users Manual e 9 with Synthesis X a RAT DemoPropAssurance Po E g File Edit View Help Douo m 2 New Open Save Traces Assurance Simulation Realizability Signals gt Requirements 6e Name Type kra Notes iA Name kina Property _ Notes The input signal for incrementing the value inc boolean E of the The input signal for dec boolean decrementing the value of the counter always forall M in 6 5 v M amp amp inc gt next v M 1 R1 G counter always forall M in 5 6 v M amp amp dec gt next v M 1 The value of the counter each inc is immediately followed by an increment of v each dec is immediately followed by a decrement of v inc and dec never
84. to open the editing windows of several items at one time or to delete more than one item at one time Multi row editing and parenthesis highlighting are provided to ease the input of properties and to make more effective their visualization Notice that all the tasks that can be per formed on signals requirements possibilities assertion traces and categories are accessible also through pop up menus that shows when the user right click with the mouse on an item the pop up menus offer also selection facilities like select all deselect all and invert selection Since as pointed out in 2 Section 2 it may be of great use to simulate a property when the results of a Property Assurance check are not of ease comprehension RATSY Requirements Analysis Tool RATSY Users Manual e 5 with Synthesis Create a new possibility Name P1 i i Property always forall Nin 5 Sh v N gt eventually v N Notes Can it be the case the counter changes value 98 Cancel 2 OK x x Create a new assertion Name Al g i Property always forall M in 5 5 v M gt v M until inc dec Indent Notes w does not change if there are no inc and dec 98 Cancel 2 OK Figure 6 Creating possibilities and assertions the user is provided with the possibility of loading an item that belongs to re quirements possibilities or assertions into Pro
85. trace The last part of the Property Simulation main window is the control and status bar located at the bottom It includes the following contents e Witness Button Pressing this button you can ask RATSY to derive a trace living up to the property and the feature requests you may have stated e Counterexample Button With a click on this button you can ask RATS Y to provide a trace contradicting the property or possible feature requests e Status At this location you can always see what RATSY is up to when doing a computation and the status of the trace and evaluation when idle Examples are Witness Counterexample VIS Error e Analysis Button A click on this button raises another second analysis win dow offering coverage information and controls as discussed in the very next section The Analysis Window The analysis window completes the information and controls of the main window For each sub formula of the property the window contains coverage statistics and RATSY Requirements Analysis Tool RATSY Users Manual e 15 with Synthesis offers controls to request for the next trace that this part should evaluate globally or finally to true or false The coverage statistics tell how often a properties part evaluates to true and false and how often this evaluation change during the evaluation of the trace These statistics are derived for the finite and infinite parts of the trace complemented by numbers for the entire trace
86. ues to don t care Not only the current state of the play but arbitrary time steps can be displayed in the automata Simply right click onto any signal in the desired time step and selects the menu item Show step in automata Specifying Design Intent When you observe undesired behavior of the system while playing a normal game you can switch into the Specify Design Intent mode by selecting the corre sponding radio button in the Game window on the bottom of the right hand side in Figure 37 The game trace can be used as a starting point to specify the desired behavior of the system You can change the value of any signal inputs and out puts in any time step to 0 1 or don t care This is done by right clicking onto the signal in that time step and selecting the corresponding menu item It is also possible to set a certain signal in all time steps to a certain value by right clicking onto the signal name in the trace The waveform color black is used for signal values that came from the game The waveform is colored in red if the signal value was changed by you The finite part and the infinite loop of the trace can be edited in the same way as in the game Unlike in the game new time steps can be inserted and existing time steps can be removed from the trace again by right clicking onto the desired position and choosing the corresponding menu item In the end the input trace and the output trace should represent the desir
87. ugh a game They are written in blue All types of messages can be enabled or disabled with the corresponding check boxes Information will be stored in the background even while a particular mes sage type is disabled When re enabling it later the messages will be displayed as if the message type was never disabled 32 e RATSY Users Manual RATSY Requirements Analysis Tool with Synthesis Integration with the Automaton Editor The following features are only available if the specification contains automata constructed with the automaton editor see Section 1 4 Figure 43 shows an example for the Automata sub window of the game The names of all automata of the specification are shown on the left side in case of Figure 43 there is only one One such name can be selected and this selected automaton is shown on the right side The current state of the play is marked with yellow in the automaton Also all edges that are still possible with the current user selection in the Game window are marked yellow If you want to traverse a certain yellow edge of the automaton in the game you can simply select this edge with a mouse click The restrictions imposed by traversing this edge are then added as additional user selections to the signals that are under control of the user in the game User selections obtained by selecting edges can be cleared again by clicking the Clear button in the Game window or by setting the corresponding signal val
88. uirements toxo Name Type Kind Notes amp Name Kind Automaton Property Notes Eenvint A r0 0 amp amp 0 amp amp startup_failed 0 nitial condition rl boolean E resource request by entity 1 Ivsysinit G g0 0 amp amp g1 0 amp amp error 0 initial condition startup_failed boolean E environment could not start up Iv sys tran 0 G never g0 1 amp amp g1 1 never more than one grant go boolean S resource granted to entity 0 Iv sys tran 1 G always error 1 gt gO 0 amp amp g1 0 no grant on error gl boolean S resource granted to entity 1 Iv sys fair O G always eventually ro 0 g0 1 eventually a grant for entity 0 error boolean S something went wrong lv sys fairl G always eventually r1 0 g1 1 eventually a grant for entity 1 Ivenvfair A always eventually TRUE no environment assumption Figure 38 The specification used for Game demo When the button Start is clicked the tool first checks if the specification is realiz able This specification is indeed realizable so the tool starts a normal game You can define values for the inputs and the tool responds with outputs that conform to the specification A possible simulation run is depicted in Figure 39 Game inputs Step1 Step2 Steps ro rl startup_failed Outputs Step1 Step2 step3 oo gl error ix Figure 39 A possible simulation run Suppose now that you are not satisfied with the behavior of the system during simulation Suppose that the origina
89. use the automaton is always kept deterministic Thus we are already finished Your automaton should now look like in Fig 36 Click Ok to close the editor You will see the formula that has been automatically generated in the remaining dialog window There are two ways in which the formula can be generated which differ in the way in which they handle the implicit dead state that has been mentioned before If the checkbox Generate dead state formula is ticked the implicit dead state will be treated just like any other state It will be encoded using state variables it will be a non accepting state and it will have a self loop labeled true If this checkbox is not ticked the dead state will not be treated as a real state of its own No state encoding will be assigned to it Instead whenever an edge which would lead to the dead state is traversed a special signal dead is asserted How ever the formula contains also a conjunct stating G dead 0 Note that both types of formulas define the same regular language Choose whatever suits your needs or your liking better but don t forget to create the signal dead in your main project if you decide to use the latter case Finally click 0k again to save the automaton On a side note The labels on the edges can also be moved To do so first select the edge with a left click Then press and hold the left mouse button on an arbitrary position along the edge If you now move the mouse to the right whil

Download Pdf Manuals

Related Search

Related Contents

Fujitsu SCENICVIEW B15-1S  MPT-H1取扱説明書 rev1.00  the Kansas Geological Survey  ださい。 メカボックス交換後は、新しい翼翼フK栓を鞭用く  FRANCINOX Manuel d`utilisation - Euroflex  Cables Direct MPN-4 mouse pad  Benq MS513 data projector  

Copyright © All rights reserved. Failed to retrieve file