The Lurette V2 User guide Verimag Research Report n TR-2004-5
Contents
1. we neal T3 real 24 17 August 2015 Verimag Page 19 24 Lurette user guide References 1 N Halbwachs P Caspi P Raymond and D Pilaud The synchronous dataflow programming language Lustre Proceedings of the IEEE 79 9 1305 1320 September 1991 N Halbwachs J C Fernandez and A Bouajjanni An executable temporal logic to express safety properties and its connection with the language lustre In ISLIP 93 Quebec 1993 N Halbwachs F Lagnier and P Raymond Synchronous observers and the verification of reactive systems In Third Int Conf on Algebraic Methodology and Software Technology AMAST 93 Twente The Nederlands 1993 Workshops in Computing Springer Verlag Erwan Jahier Nicolas Halbwachs and Pascal Raymond Engineering functional reguirements of reactive systems using synchronous languages In International Symposium on Industrial Embedded Systems 2013 SIES 13 Porto Portugal 2013 Erwan Jahier and Pascal Raymond Lutin Reference Manual Https www verimag imag fr DIST TOOLS SYNCHRONE lurette doc lutin man pdf Erwan Jahier Pascal Raymond and Philippe Baufreton Case studies with lurette v2 Software Tools for Technology Transfer 8 6 517 530 nov 2006 Pascal Raymond Yvan Roux and Erwan Jahier Lutin a language for specifying and executing reactive scenarios EURASIP Journal on Embedded Systems 2008 24 Lure2. c5 f VAR CIO iz The coverage is a function from asut an oracle e a set of runs rif files 24 Lurette user guide The header contains information about the sut and the oracle we measure the coverage of SUT and ORACLE Then comes the set of runs that have been performed on them RIF Finally comes the list of coverage variables and their status indication if there had been true at least once during a run t meaning covered When no coverage file is specified Lurette creates such a file using as coverage conditions all the Boolean outputs of oracles the first one excepted as it is used to hold the test verdict If one wants to remove a coverage condition without changing the oracle profiles it suffices to remove or comment the corresponding line in this coverage file When the SUT or the oracle changes the coverage is reset One can also force the coverage resetting using the reset cov file tru option in batch mode or the reset_cov_file true commande in interactive mode cf also the check ri f bacth tools in Section 3 7 24 Lurette user guide 3 Third party tools used by lurettetop Some of the lurettetop commands actually rely on stand alone executables that can be used in command line or scripts We present them briefly in the following When strange messages are displayed by lurettetop it migth be easier to understand what happens with those stand alone tools For example imagine you wa
3. no local var Do not display environment local variables in sim2chro direct Set the direct mode old mode Unset the direct mode ocaml version Display the version ocaml version lurette was compiled with and exit version Display the version and exit help Display this list of options If a resource file exists in the current directory lurettetop will first interpret its content and then interpret the command line batch options and thus override the lurette_rc commands The batch commands generates a lurette batch file with current test parameters 2 4 Oracle coverage In Lurette in order to define the coverage of an oracle one just needs to add additional Boolean variables to its output profile By convention the first output holds the oracle result and the following outputs define the oracle coverage Lurette updates the coverage rate from one execution to another via a file This coverage rate is reset each time either the oracle or the SUT is modified cf Section 2 4 The coverage file cov Lurette maintains the coverage information via a cov file which looks like this SUT v6 heater_control lus main ORACLE v4 heater_control lus not_a_sauna ORACLE v6 heater_control lus not_a_fridge RIF test rif0 generated at 16 28 15 the 18 4 2011 the coverage rate is 50 0 RIF test rif0 generated at 16 29 20 the 18 4 2011 the coverage rate is 60 0 VAR cl t VAR c2 f MARES it VAR c4 t VAR
4. An experimental debugger for Lustre V6 and Lutin 1dbg shell ldbg help This is ldbg Version 1 54 al22bf0 type man for a small on line manual Usage ocaml lt options gt lt object files gt script file arguments options are absname Show absolute filenames in error messages I lt dir gt Add lt dir gt to the list of include directories init lt file gt Load lt file gt instead of default init file labels Use commuting label mode no app funct Deactivate applicative functors noassert Do not compile assertion checks nolabels Ignore non optional labels in types noprompt Suppress all prompts nopromptcont Suppress prompts for continuation lines of multi line inputs nostdlib Do not add default directory to the list of include directories ppx lt command gt Pipe abstract syntax trees through preprocessor lt command gt principal Check principality of type inference rectypes Allow arbitrary recursive types short paths Shorten paths in types stdin Read script from standard input strict seguence Left hand part of a seguence must have type unit unsafe Do not compile bounds checking on array and string access version Print version and exit vnum Print version number and exit w lt list gt Enable or disable warnings according to lt list gt 24 Lurette user guide lt spec gt enable warnings in lt spec gt lt spec gt disable warnings in lt spec gt lt spec gt enable warnings in lt
5. EK REELS BRE DS 11 a2 The Litn interer litany o s ps e foe ee eo ee ee ee c 11 3 3 The Lustre V4 interpreter ecexe FF I yg 12 34 The Liste Volmenpietet Las ALI EJ opa e ee ee BAe a 12 3 3 Interactive simmiaton luctole oe set eda Ve fe ee a FU RW E 12 3 6 Gnuplot based data visualisation gnuplot rif 13 3 7 Post mortem coverage analysis Check rif D G 13 3 8 An experimental debugger for Lustre V6 and Lutin 1dbg 14 4 Installation process 16 5 A small tutorial 17 A RIF Reactive Input Format 18 Connecting to Lurette using sockets 21 Bel The socket plugin API a 50208 GR RG EG FU GR A RG 21 Be Tie hosi TOMA e sio RR HN FRON eS 22 C Connecting to Lurette using shared libraries DLL SO 24 24 Lurette user guide 1 Lurette Principles 1 1 Introduction The functional testing of reactive systems raises specific problems We adopt the usual point of view of synchronous programming considering that the behavior of such a system is a sequence of atomic reactions which can be either time triggered or event triggered or both Each reaction consists in reading inputs computing outputs and updating the internal state of the system As a consequence a tester has to provide test seguences i e seguences of input vectors Moreover since a reactive system is generally designed to control its environment the input vector at a given reaction may depend on the p
6. imag fr Lustre V6 html 24 Lurette user guide 1 4 Oracle Coverage When performing functional testing structural coverage criteria are relevant to give insights about whether or not enough tests have been done We need coverage criteria attached to requirements Consider for instance the following property which expresses that when a threshold is exceeded and when the system is in its nominal mode then an alarm must be raised T gt 100 and nominal gt Alarm There are several ways for the SUT to satisfy this property 1 T can be smaller than 100 or 2 the system can be in a degraded non nominal mode 3 otherwise Alarm must be true From the coverage point of view it is obviously the latter case that is interesting Its seems fair to consider that this oracle is not covered as long as no simulation has been run where T gt 100 and both nominal and Alarm are true The case T lt 100 is also interesting to cover but can be attached to a property related to the absence of false alarms Hence we define the coverage of an oracle as a set of Boolean conditions A run or a trace of the SUT is a seguence of the SUT input output vectors generated during a simulation The oracle coverage rate of a set of runs is the rate of coverage conditions that have been true at least once during those runs The coverage of a property is arguably part of its specification If it is not the case the persons in charge of formalizing reguirements into or
7. 4luciole Call Luciole the provide inputs h help help Display this message more Show hidden options for dev purposes 3 3 The Lustre V4 interpreter ecexe The Lustre V4 compilation tools chain rely on so called Lustre expanded code or ec for short ec stands for expanded code XXX un xfig decrivant la chaine d outil lustre V4 avec lus2ec ec2c ec2ec exexe lesar lt lurettetop gt add_rp sut v4 heater_control lus heater_control When adding a reactive programs flagged the the v4 option Lurettetop actually uses ecexe to interpret the ec generated by the 1us2ec compiler 3 4 The Lustre V6 interpreter lus2lic 3 5 Interactive simulation Luciole Sometimes it s useful to have interactive test sessions typically be before writing a first Lutin environment for a SUT shell luciole h nil 24 Lurette user guide 3 6 Gnuplot based data visualisation gnuplot rif shell gnuplot e1f help gnuplot rif options lt f gt rif Generates a lt f gt gp file such that gnuplot can plot the rif file gnuplot rif try to read the content of a file named gnuplot rif in the current directory With something like hide T hide totox It will ignore all I O which names begin by toto as well as the variable T If you write in this file something like show xx it will show show only I O beginning by xx With plot_range 12 42 it will plot data from step 12 to 42 o
8. Comments Single line comments are introduced by the two character and terminated by a new line Multi line comments are introduced by the two characters and terminated by the two characters Pragmas Pragmas are special kinds of comments that migth or not be taken into account by tools that reads RIF data One line pragmas have the form pragma_ident and multi line pragmas the form pragma ident The most common pragmas used by verimag tools are using BNF notation inputs var name var type or e inputs var name var type to declare the list of input variable names and types outputs var name var type or ffoutput var name var type to declare the list of output variable names and types locals var name var type HO or locs to indicate that the following data correspond to local variables to declare the list of local variable names and types outs to indicate that the following data correspond to output variables step int to indicate that a new step is starting and that the following data correspond to input variables Note that those pragmas are necessary for RIF file viewers such as sim2chro and gnuplot rif to work properly A RIF file example is provided in Figure it corresponds to the timing diagram of Figure seed 97040004 program lurette chronogram degradable sensors luc inputs ves reali TI reall
9. EBNF the syntax grammar is the following 24 Lurette user guide Welles WU Slim Mao gt lis O GIP orata into inputi Ss Ea lt s gt i Moveroll Wate reed Jj T resi lt siuslag een i WeeedLW rec A 4 Ji Here is an example with 3 inputs and 3 outputs Soci evclolie 127 50 0 Al Sock joe 2999 input EXE100BA_Pannel_OnOff bool input EXE101MN_Panne2_OnOff bool input EXE100BA_Pannel_Valeur real output N1 501MT Mes mV N1 real output N1 502MT Mes mV N1 real output N1 503MT Mes mV N1 real The optionnal string in the I O declaration list is used to make a mapping between the variable names used by the SUT and by Lurette is ever their differ Socia do FORO sock_port 2999 input EXE100BA_Pannel_OnOff EXE100BA Pannel_OnOff bool input EXE101MN_Panne2_OnOff EXE101MN Panne2_OnOff bool input EXE100BA_Pannel_Valeur EXE100BA Pannel_Valeur real output N1 501MT Mes mV N1 N1_501MT Mes_mV_N1 real output N1 502MT Mes mV N1 N1_502MT Mes_mV_N1 real output N1 503MT Mes mV N1 N1_503MT Mes_mV_N1 real For example EXE100BA Pannel OnOff is the Lurette nane and EXE100BA Pannel OnOff is the name used by the SUT Most of the time we use in Lurette the variable name used by the SUT However in this particular example the SUT variable name uses semi colons which is not a valid variable name for Lurette We do have a C liosi parser that a
10. acles are in the best position to define the coverage at the same time cf Section 2 4 for a more detailled description of how coverage is handled in Lurette 1 5 The Lurette workflow The design of the system its oracles and its stimulus generators is not a linear process Several iterations are necessary that are described below and outlined in Fig 1 ved valid and nominal gt T lt 100 Wrong or imprecise spec bug design coding Specifications gt gt Car problem gt Oracles mm gt Coverage vasi gt Environnements ok ko extraction formalisation translation refinement scenario Figure 1 The Lurette iterative process loops Oracles and environments of the SUT are extracted from heterogeneous specifications When an oracle is invalidated it can be due to a design error a coding error or to a wrong or imprecise specification Once the system is running without invalidating oracles in order to improve the coverage rate the tester needs to refine test scenarios 24 Lurette user guide Refining the SUT When an oracle is violated it can be of course because of a design or coding error which results in a erroneous SUT Detecting such incorrect behaviors of the SUT is indeed the original motivation of all this infrastructure Refining oracles An oracle violation can also be due to a wrong fo
11. allenge to automate the testing process is to able to automate the generation of realistic input sequences to feed the SUT In other words we need an executable model of the environment which inputs are the SUT outputs and which outputs are the SUT inputs The environment is also a reactive system that executes in closed loop with the SUT It can be very versatile or underspecified This motivated the design of Lutin 7 a language to program stochastic reac tive systems and environment models For more information on Lutin please refer to the Lutin language reference manual 5 A tutorial is also available http www verimag imag fr DIST TOOLS SYNCHRONE lurette lutin tuto html html http www verimag imag fr DIST TOOLS S YNCHRONE lurette doc lutin man pdf http www verimag imag fr Lutin html 1 3 Oracles The test decision is a deterministic process which can be automated using a formalization of SUT expected properties predicate over traces By convention a Lurette oracle is a program that returns as first output a Boolean that formalizes one or several requirements Lurette reports a property violation each time one oracle returns false As expected properties of reactive systems often involve time a language where time is a first class concept like Lustre 1 is a sensible choice Moreover Lustre allows formalizing any safety property 2 http www verimag imag fr The Lustre Toolbox html Lustre V4 http www verimag
12. commande check rif 24 Lurette user guide Cet utilitaire utilise un oracle et un fichier rif g n r lors d une pr c dente session de test pour calculer o i mettre jour la couverture fonctionnelle associ e cet oracle La commande check rif help expligue tout ce gu il y a savoir sur cet outil shell check rif help Usage check rif options ec lt file gt ec lt Rif File name to check gt Performs post mortem oracle checking using ecexe The set of oracle Inputs should be included in the set of the RIF file inputs outputs At the first run the coverage information is stored updated in the coverage file cf the cov option to set its name The variables declared in this file should be a subset of the oracle outputs If the coverage file does not exist one is is created using all the oracle outputs If not all those outputs are meaningfull to compute the coverage rate one just need to delete corresponding lines in the coverage file The format of the coverage file is straightforward but deserves respect Options are ec lt string gt ec file name containing the RIF file checker a k a the oracle cov lt string gt Override the default coverage file name lt oracle name gt cov by default reset cov reset the coverage rate to 0 before running stop at error Stop processing when the oracle returns false debug set on the debug mode help Display this list of options 3 8
13. e test length 10 precision 2 seed chosen randomly verbosity level 0 rif file name lurette rif overwrite rif file no coverage file name lurette cov do we stop when an oracle returns false no display local var no lt lurette 2 gt 2 2 The resource file luretterc When lurettetop is launched it first reads the content of the resource file named lurette_rc in the current directory The syntax of this file is just the one of interactive commands described by the online manual man displayed above lt lurette gt add rp sut v6 heater_control lus heater_control lt lurette gt add_rp env lutin env lut main lt lurette gt set_test_length 1000 2 3 The batch command interpreter lurettetop can also be used non interactively using the batch option In order to set the various parameters you can either seta luretterc resource file in your current directory or use command line options The list of options can be obtained using the help option when invoking lurettetop shell lurettetop help usage lurettetop lt options gt lurettetop is a top level loop that let one use lurette Type help and or man at the prompt for more info launch lurettetop help to see the available options reactive program lt string gt rp lt string gt To specify a reactive program to be used in the test session one should use a string with the following format machine_kind language
14. e before the test is launched The binding between programs is done by name 3 2 The Lutin interpreter Lutin shell lutin help 24 Lurette user guide usage lutin options lt file gt lutin help n m node main lt string gt Set the main node version version Print the current version and exit Set the verbose level to 1 vl lt int gt Set the verbose level gnuplot gp call gnuplot rif to display data type rif guiet g only outputs display only outputs on stdout i e behave as a rif input file o lt string gt output file name cL lib lt string gt Add a dynamic library where external code will be searched in seed lt int gt Set a seed for the pseudo random generator rar a in the gnuplot window to refresh it boot Perform ther first step without reading inputs max steps l lt int gt Set a maximum number of simulation steps to perform step inside si Draw inside the convex hull of solutions default step edges se Draw a little bit more at edges and vertices step vertices sv Draw among the vertices of the convex hull of solutions precision p lt int gt Set the precision used for converting float to rational default 2 locals loc Show local variables in the generated data ocaml ocaml Generate ocaml glue code that makes it possible to call the lutin interpreter from ocaml with the current set of arguments luciole 2c
15. erimaG The Lurette V2 User guide Erwan Jahier Verimag Research Report n TR 2004 5 Initial version 12th March 2004 Last update 17 August 2015 Software Version 1 56 Reports are downloadable at the following address http www verimag imag fr Unit Mixte de Recherche 5104 CNRS Grenoble INP UJF Fourler CD PS Centre quation 2 avenue de VIGNATE F 38610 GIERES tel 33 456 52 03 40 fax 33 456 52 03 50 http www verimag imag fr De 7 Keywords Reactive systems validation automatic test case generation Lurette Lustre Lutin Reviewers Nicolas Halbwachs How to cite this report techreport TR 2004 5 title The Lurette V2 User guide author Erwan Jahier institution Verimag Research Report number TR 2004 5 year 2004 Lurette user guide Contents 1 Lurette Principles 2 LI E 2 L2 Environment ce ea NEF FFAN NENN a 2 LI TES uu Ge lea E de ek HO A es es Rh eh hos Sw BE n 2 La Orce Covent un eee Saw ee Ae eee Ee Se oe SE MB 3 VS The Lurette warkilow oa il e e ee a BARD 3 2 The Lurette toplevel commands interpreter lurettetop 5 2 1 The interactive command interpreter Hu e 5 22 The resource file luretterc si 0840004 WM Ud ee be Cy A EN 6 2 3 The batch command interpreter s crc a ak OS ERS RA G 6 ZA acl coverage i RA MAE A n 9 3 Third party tools used by lurettetop 11 31 A summary of tools and dataflow gt lt il
16. exceeds 100 degrees when the system is in the nominal mode and the validity bit associated to its sensor is 1 One outcome of the project is that the Lurette tool and methodology was actually helpful for debugging and refining requirements Refining scenarios When the coverage is not complete we must enrich the set of possible behaviors of the environment with new scenarios Note that new scenarios may lead to properties violations which lead to changes in the SUT or in oracles and changes in the SUT may change the coverage in turn 24 Lurette user guide 2 The Lurette toplevel commands interpreter lurettetop 2 1 The interactive command interpreter Lurette handles the test harness by reading test parameters executing all the reactive systems in turn SUT environment oracles computing reguirements coverage and displaying a test report It does not impose the use of Lustre or Lutin The reaction steps can be either time triggered event triggered or both Presentations of Lurette can be found in 4 6 The interactive command interpreter is named lurettetop The first command you can try is the man or m for short that will display a small online manual shell lurettetop lt lurette l gt man This is Lurette Version 1 54 8eb7lec lt lurette l gt Once lurettetop has been launched a prompt is printed waiting for user gueries One first need at least to set the sut system under test and the environment f
17. exists without tring to invent a new name 00 bateh Start the testing process directly without prompting go go step Run lurette step by step socket inet addr Set the socket address socket io port Set the socket io port socket err port Set the socket error port show step Set on the show step mode do not show step Set off the show step mode verbose Set the verbose level reactive Set on the reactive mode r prompt Replace the default prompt extra source files Set the EXTRA SOURCE FILES environment variable extra libs Set the EXTRA_LIBS environment variable extra libdirs Set the EXTRA_LIBDIRS environment variable extra includedirs Set the EXTRA_INCLUDEDIRS environment variable step mode Set the step mode used to perform the step delay env outputs Delay the outputs of the environements before transmitting them to the oracles luciole Call lurette via luciole pre processor Pre processor for Lucky files e g cpp 24 Lurette user guide PP prefix A string to append before the call to lurette e g usr bin times tmp dir Use that directory to put temporary files log Redirect stdout to a log file lurette_stdout log gnuplot Call gnuplot no gnuplot Do not call gnuplot ngp sim2chro Call sim2chro no sim2chro Do not call sim2chro ns2c local var Display environment local variables in sim2chro on
18. file node where machine kind can be sut oracle or env language can be v4 to use the Lustre V4 programs v6 to use the Lustre V6 programs lutin to use the Lutin programs ocaml to use the Ocaml programs ocaml Tec to use the ec programs ec_exe to use a standalone executable obtained from an ec file ex_exe file should be an existing file compatible with the compiler field node should be a node of file if meaningful or empty 24 Lurette user guide ocaml In the ocaml mode the file can be an f ml file or a f cmxs file If an ml file is provided lurettetop try to generate a cmxs file from it If your caml program depends on library or on other files please generate the f cmxs file by yourself cf the ocaml documentation ec_exe In the ec_exe mode lurette suppose that file ec has been compiled into an executable that is named file for instance via ec2c loop That executable must read write its I O using the RIF convention The rationale for that mode is to be able to deal with Lustre programs that use C code The file ec is just used to retrieve the I O var names and types actually An alternative format is the following machine_kind socket sock_addr port where machine kind is as above sock_addr is a valid internet adress port is a free port on sock_addr The lurettetop process play the role of the client exchanges on the socket
19. fine MAX BUFF SIZE 2048 To be set with care define SOCK_ADDR 127 0 0 1 define SOCK_ PORT 2000 typedef int _bool A little program with 3 inputs and 3 outputs that dialogs with lurette on a socket int main ine at 0 oa aste OR char buff MAX_BUFF_SIZE int sock sockfd newsockfd clilen struct sockaddr ini serv_addr cli addr The program Inputs int eye bol dop double char b_char used for reading booleans on the socket The program Outputs int x 0 _bool y 0 double z 0 0 Socket administration ifdef _WINSOCK WSADATA WSAData 24 Lurette user guide WSAStartup MAKEWORD 2 0 amp WSAData fendif sockfd socket AF INET SOCK_ STREAM 0 alu e oyelienol lt 10 jr Maracas perineo ce serv_addr sin family AF_INET serv_addr sin_addr s_addr inet_addr SOCK_ADDR serv_addr sin port htons SOCK_PORT if bind sockfd struct sockaddr amp serv_addr sizeof serv_addr printf Error when binding s d n SOCK ADDR SOCK PORT exit 2 listen sockfd 5 clilen sizeof cli_addr newsockfd accept sockfd struct sockaddr amp cli_addr amp clilen 1 newsockfd lt 0 printf Error on accept sock newsockfd Make sure that the program uses a for reals and not a_ setlocale LC ALL English sending I O declarations memset buff 0 MAX BUFF_ SIZE sprintf buff inputs nx int ny bool n z real n n multi line rif decl send soc
20. ields like that your shell prompt lurettetop lt lurette gt add_rp sut v6 heater_control lus heater_control lt lurette gt add_rp env lutin env lut main lt lurette gt add_rp oracle v6 heater_control lus not_a_sauna lt lurette gt add rp oracle ec not_a_sauna ec And then the testing process can start lt lurette gt run sre testing cce Equivalently you can directly set values at the command line your shell prompt lurettetop rp sut v6 heater_control lus heater_control rp oracle v6 heater_control lus not_a_sauna rp env lutin env lut main lt lurette gt run testing You migth also want to try the info command i for short to get the values of the test parameters and the h help command to obtain the list of possible commands lt lurette 2 gt Here and in the following shell is the shell prompt lt lurettetop gt is the lurettop prompt Let s paraphrase what this small online help says shell lurettetop lt lurette l gt man add rp XXXX il faudrait un truc comme ca ca y est dans ldbg gt Merger As this manuals say you can get the list of available commands with help or h Another very useful command is info or i that returns the current values of test parameters shell lurettetop lt lurette gt info 24 Lurette user guide This is Lurette Version 1 54 8eb7lec lt lurette 1 gt The current test parameters are sut env oracl
21. k buff Gnt selena sprintilbuff outputs asint brbool esfpeal mn yy single line rif decl Just for fun send sock buff int strlen bu f f 0 for i l i lt 10 1 1 The main loop 1 Reading inputs memset buff 0 MAX BUFF_ SIZE rc recv sock buff MAX BUFF_ SIZE 0 arnie lt 0 1 pPEintE EErors cannot read on socket exit 2 fF Seca gui WE wie lie Gel Bo Char Gi Translate char into int if b_char 0 b ehar f b_char F b 0 IE se char RO Muda ME a AR DSE 2 Computing the outputs using the inputs scel ai by LL y O else y ay fs ec 20 1 i 3 NE Tn odo memset buff 0 MAX BUFF_ SIZE sprint butt Sd Sa ale wn a DR el send sock buff int strlen buff 0 A small debug printf to see what s going on printf istep 2d m d id SE 4outs a sd Sin 1 a b Cy amp Yi sprintt bunt ipo Va Sendi SOCk buf nE ste lente 0 return 0 B 2 The liosi format Liosi stands for Lurette input output socket interface The objective of the liosi format is to define in a single file all the necessary information to be able to connect any reactive system to Lurette using sockets A liosi file contains the following information sock_addr the IP adress of the machine where the SUT runs e sock_port the port number of the socket input SUT inputs name and type output SUT outputs name and type In
22. llows to connect easily any SUT that can be interfaced with C available on demand 24 Lurette user guide C Connecting to Lurette using shared libraries DLL SO Its works but it s not documented yet XXX start me 24
23. nly With dynamic window_size 56 will show only the last of 56 steps of the simulation 40 by default If one show statement is used all hide statements are ignored If several plot_range or window_size are used the last one win All these values can be overriden by setting options Command line options are handled afterwards no display generate the gp file without launching gnuplot dyn dynamically display the end of the rif file size lt s gt set the size of the sliding window in dyn mode min lt min gt only display steps gt min ignored in dyn mode max lt max gt only display steps lt max ignored in dyn mode nogrid remove the grid useful with dyn hide var lt string gt hide a variable one can use the wildcard x show var lt string gt show a wildcard hided variable wxt launch gnuplot with the wxt terminal default x11 launch gnuplot with the X11 terminal jpg output in a jpg file pdf output in a pdf file ps output in a B amp W post script file cps output in a color post script file eps output in a color encapsulated post script file latex output in a latex file Vv set on a verbose mode h display this help message 3 7 Post mortem coverage analysis check ri Lurette met jour la couverture des test par l entremise du fichier cov au fur et mesure que les tests se d roulent Mais il est galement possible s utiliser un petit utilitaire en ligne de
24. nt to test with Lurette a Lustre V4 program that reguires several environment programs with several oracles it migth 3 1 A summary of tools and dataflow Lurette handles the test harness by reading test parameters executing all the reactive systems in turn SUT environment oracles computing reguirements coverage and displaying a test report Figure 2 outlines what happens during a test run l oracle Figure 2 Lurette data flow At each step each orange box is activated from left to right A Luciole process is used only if necessary i e if a SUT or an ENV input is missing At least one SUT or one ENV is necessary The sim2chro process can be launched from Luciole or post mortem from the Lurette UI via the generated rif file The environment outputs are the SUT inputs and SUT outputs are the environment inputs In order to be able to start such a looped design one entity have to start first The choice has been made that the environment will This means that a valid environment for Lurette is one that can generate values without using its input at the first instant If one input is missing to the SUT or to its environment a tcl based GUI Luciole is launched to generate the missing variables The Luciole process is started before the environment ones The SUT the environment and oracles can be splitted into several reactive programs Each variable should be produced exactly by one program This is checked by Lurett
25. revious outputs As a consequence input sequences cannot be produced off line and their elaboration must be intertwined with the execution of the system under test SUT Finally in order to decide whether a given test succeeds or fails the sequence of pairs input vector output vector can be provided to an observer 3 which acts as an oracle at each reaction Let us illustrate this process with a very simple example consider a device whose role is to regulate the water temperature of a tank by opening or closing a gate that controls the arrival of hot water A reaction consists in sampling the water temperature comparing it to the target temperature and sending an order to the gate In a realistic input sequence the temperature is assumed to increase at some rate when the gate in open and to decrease when it is closed Hence the input at a given reaction depends on the output sent at the previous reaction The property to be checked could be that if the target temperature did not change during a given delay the temperature should belong to a given interval around the target temperature This global property of the combination system environment can be checked after each reaction by an observer which must have an internal memory to count the delay from the last target change Moreover from this property coverage point of view we want to generate sequences where the target temperature do not change too often 1 2 Environment The main ch
26. rmalization Despite the fact that seguence recognizers oracles are much simpler to develop than seguence generators SUT they are still the result of a human work and thus exposed to errors Refining ambiguous requirements Lurette can also detect ambiguous requirements when they are interpreted differently by the SUT and the oracle designers It happened quite frequently during the project Refining inconsistent requirements Formalizing requirements in a language such as Lustre that is equipped with a model checker allows to detect inconsistencies i e the absence of correct behaviors Refining imprecise requirements Another reason that results in invalidated oracles is when they are based on imprecise requirements One typical case encountered in the project was a requirement formulated as follows when x exceeds the threshold t the alarm a should be raised In a distributed system like the one of COMON where sub systems communicate over buses and networks such a requirement will be immediately violated if interpreted literally One should permit some reaction delay and specify its bounds Refining incomplete requirements Another very common source of oracle violations is a lack of com pleteness A typical example also encountered during the project is a requirement that states that the temperature of tank t should never exceeds 100 degrees whereas the correct requirement was the tem perature of tank t should never
27. should respect the RIF Reactive Input Format Hence to sum up we currently support lt sut env oracle gt lutin prog node For lutin programs lt sut env oracle gt v6 prog node For lustre V6 programs lt sut env oracle gt v4 prog node For lustre V4 programs lt sut env oracle gt ec prog For lustre expanded code programs lt sut env oracle gt ec_exe prog For lustre expanded code programs that have been compiled lt sut env oracle gt socket addr port For reactive programs that read write on a socket lt sut env oracle gt socket_init addr port Ditto read I O init values before the first step Examples sut v6 controler lus main env lutin train tgv oracle socket 127 0 0 0 2042 sut lt string gt File name of the system under test works with old mode only sut lt string gt sut cmd lt string gt Command that launches the system under test works with old mode only sut cmd lt string gt oracle cmd lt string gt Command that launches the oracle works with old mode only oracle cmd lt string gt main sut node lt string gt Main node name of the system under test works with old mode only msn lt string gt main env node lt string gt Main node name of the environment meaningful for lutin only works with o men lt string gt oracle lt string gt File name of the oracle works with old mode only oracle lt string gt main oracle node lt s
28. spec gt and treat them as errors lt spec gt can be lt num gt a single warning number lt numl gt lt num2 gt a range of consecutive warning numbers lt letter gt a predefined set default setting is a 4 6 7 9 27 29 32 39 41 42 44 45 warn error lt list gt Enable or disable error status for warnings according to lt list gt See option w for the syntax of lt list gt Default setting is a warn help Show description of warning numbers dsource undocumented dparsetree undocumented dtypedtree undocumented drawlambda undocumented dlambda undocumented dinstr undocumented lt file gt Treat lt file gt as a file name even if it starts with help Display this list of options help Display this list of options 24 Lurette user guide 4 Installation process XXX start me 24 Lurette user guide 5_ A small tutorial ccc 24 Lurette user guide A RIF Reactive Input Format RIF stands for Reactive Input Format It is the format used by the synchronous Verimag tools for writing and reading sequences of input and output data vectors We recall in this section what this format looks like Data A RIF file is a sequence of data values separated by spaces newlines horizontal tabulations carriage returns line feed and form feeds A data value can be either an integer a floating point or a Boolean t T or 1 stands for true f F or 0 stands for false
29. tring gt Main node name of the oracle works with old mode only man lt string gt sut compiler lt string gt lv4 lv6 scade Compiler used for the sut works with old mode only oracle compiler lt string gt lv4 lv6 or scade Compiler used for the oracle works with old mode cov file lt string gt file name coverage info will be put into test length lt int gt Number of steps to be done l lt int gt currently 10 precision lt int gt number of digit after the dot used for floating points p lt int gt 24 Lurette user guide fair Compute the polyhedra volumes before drawing compute poly volume more fair but more expensive thick draw lt int gt Number of draw to be done in each formula td lt int gt at each step currently 1 draw inside lt int gt Draw on the edges of the convex hull of solutions draw edges lt int gt Draw on the edges of the convex hull of solutions draw vertices lt int gt Draw among the vertices of the convex hull of solutions draw all formula Tries all the formula reachable from the current state draw all vertices Tries all the polyhedra vertices seed lt int gt Seed the random engine is initialised with seed lt int gt dbg debug mode to debug lurettetop ldbg use the lurette debugger output lt string gt Set the output file name currently lurette rif o lt string gt overwrite output Overwrite lurette rif if it
30. tte user guide B Connecting to Lurette using sockets B 1 The socket plugin API Lurette entities SUT oracles environments can also be a stand alone program that reads and writes its inputs outputs on a socket Of course such programs ougth to respect a precise protocol that we describe below 1 First it must connect to an inet socket defined by an address and a port using the listen command 2 Then it must write its input variable names and types that will be received from the lurette process using the RIF convention 3 Then it must write its output variable names and types that will be send to lurette process using the RIF convention 4 Then it enter a loop where it reads its input on the socket in their declaration order e writes its output on the socket in their declaration order In order to stop that loop and inform lurette it wants to stop playing the program just have to send the quit command Here a small but complete example of a C program that is able to communicate with Lurette and that is part of its non regression test suite include lt stdlib h gt include lt stdio h gt include lt sys types h gt include lt signal h gt finclude lt locale h gt ifdef _WINSOCK finclude lt windows h gt include lt process h gt pragma comment lib Ws2_32 lib else include lt sys socket h gt include lt netinet in h gt include lt netdb h gt fendif de
Download Pdf Manuals
Related Search