Verimag Manual The aadl2sync User Guide
Contents
1. needs_a_processor_f cpu_a_processor_s cpu_a_processor_f Figure 2 A timing diagram obtained from a simulation of multitask aadl The scheduler schedule multitask lus le was generated by aadl2sync version 0 eduling vars gen fake body o bin aadl2sync show multitask multitask aaxl on peouvou the 29 6 2007 at 14 50 11 include fillme_multitask_types lus include fillme_multitask_const lus interuption generator node timer const period int qs_tick bool returns bool var cpt pcpt int let pept period gt pre cpt cpt if trig then period gs tick then pcpt 1 else pept pcpt 1 and qs_tick trig else if trig true gt tel returns node rising_edge x bool y bool let y tel false gt x and not pre x node first_rising_edge x reinit bool y x becomes true for since the beginning var EDIS VAr iS returns y bool is true when the first time or the last reinit used to encode a 2 state automaton y_has_been_emitted bool let y falge gt if not pre y_has_been_emitted and rising_edge x then true else if pre y_has_been_emitted and reinit then false else false y_has_been_emitted false gt if not pre y_has_been_emitted a2. ck1 a210101110 T T ck2 I 0 0 0 1 0 Figure 1 Two processes running on quasi synchronous clocks The important property of quasi synchronous composition of processes is that each process is guar anteed to miss at most one sample of the other s output Hence programs that are designed to be robust to clock drift if they read programs output in registers for example have the same behavior with quasi synchronous or synchronous clocks Using quasi synchronous clocks allow one to check that robustness for AADL models An AADL component to Lustre node mapping Basically the translation consists in mapping AADL components to Lustre nodes where the input output ports of components correspond to the input output of nodes and where node calls directly result from component wiring connections Since we focus on functional properties we will safely ignore in our translation most of the hardware components We also ignore most properties as they generally concern non functional aspects Nodes have additional inputs for carrying the oracles of their sub nodes Those oracles are controlled by a scheduler that is described in Section 4 More details about this component to node mapping is given in the following Section 3 The AADL component to Lustre node mapping AADL components are made of a Type and each Type is optionally associated to one or several Imple mentation s A compone
3. 5 E Jahier and P Raymond The Lucky Language Reference Manual Technical Report TR 2004 6 Verimag 2004 www verimag imag fr synchron tools html 6 1 3 6 R Milner Calculi for synchrony and asynchrony TCS 25 3 July 1983 1 7 SAE Architecture Analysis amp Design Language AADL AS5506 Version 1 0 SAE Aerospace November 2004 1 25
4. 30 and 1 lt in_min_max21 and in_min_max21 lt 5 and 1 lt in_min_max22 and in_min_max22 lt 5 and E 10 lt in min max23 and in_min_max23 lt 30 and rue tel 25 7 A test session using Lurette 8 A formal proof session using Lesar 9 The currently supported AADL subset Not all AADL concepts are supported Here is an hopefully exhaustive list of concepts that are supported and not supported by the current version of aadl2sync As the terms of components and features have a precise meaning in AADL we use in the following the hazy term of concept to distinguish what is and what is not supported by the tool 9 1 Ignored concepts Some concepts are ignored in the translation which means that they can appear in the AADL model without breaking the tool e processors the fact that several processes run on the same processor is taken into account though e memory e buses e flows most properties except the ones cited above 1 the base literal for integers base 10 is assumed TE e the time unit i e one should not use different time units Among those ignored concepts note that taking into account processors memory flows and most properties would definitely be useless for our purposes validating the functional part of the model via simulation and formal verification Concerning the other items flagged by a 1 in the contrary some could be taken into account at least par
5. An Actuator a_processor processor A_Processor IMPL a process process A Process IMBL connections data port a_process 01 gt slow_cmd 1 data port a _process 02 gt fast_cmd 1 properties Actual_Processor_Binding gt reference a_processor applies to a_process end multitask IMPL device An_Actuator features I in data port int end An_Actuator processor A Processor end Processor processor implementation A_Processor IMPL end Processor IMPL process A_Process features O1 out data port int 02 out data port int end _ Process subcomponents s thread SlowThread f thread Fastihread connections data Port 1210 gt So lp data port GIO gt ET data port s 0 gt Ol data port E O gt 027 end A_Process IMPL thread SlowThread features I in data port int O out data port int properties Dispatch_Protocol gt Periodic Period gt 15 ms Compute Execution Time gt 1 ms 12 ms end SlowThread thread FastThread features I in data port int O out data port int properties Dispatch_ Protocol gt Periodic Period gt 110 es Compute_Execution_Time gt 1 ms 6 ms end FastThread data int end int process implementation A_Process IMPL This file can be found in the examples multitask directory of the distribution Launch make demo to generate a executable simulation of it Figure 2 illustrates XXX Note that thrl_activateis true every 4
6. V4 23 25 1 Introduction Architecture Description Languages ADL aim at defining systems by describing jointly software and hardware components and their interactions ADL can describe functional interfaces to components and non functional aspects reliability availability timing responsiveness etc The objective is to be able to perform various analysis schedulability sizing analysis safety analysis very early in the development process AADL Architecture Analysis and Design Language is one such ADL that specifically targets real time embedded systems It lets one describe the structure of such systems as an arborescent assembly of software components mapped onto an execution platform The leaves of that arborescent description are made of component interfaces that are left un implemented Given an AADL model and implementations for the component leaves the aadl2sync allows one to perform automatically simulation and formal verification This is done by translating the AADL model into the Lustre programming language for which simulation and formal verification tools exist This tool chain allows one to focus on functional properties far before machine code generation and deployment phases The main difficulty in this translation is to model intrinsically non deterministic and a synchronous AADL descriptions into a synchronous language To do that we use techniques based on sporadic activa tion condition stuttering 6 input a
7. clk bool defl multitask_int xl multitask__int returns yl multitask_ int let yl defl gt pre if clk then x1 else yl tel End of node barrier_multitask__SlowThread Condact multitask__SlowThread node condact_mult itask__SlowThread clk bool defl multitask_ int returns yl multitask_ int var x1_when_clk let x1_when_clk xl multitask__int Ne multitask__int when clk xl when clk yl if clk then current multitask__SlowThread x1_when_c1k else defl paa MN tel End of node condact_multitask__SlowThread Barrier of multitas __FastThread node barrier_multitask__FastThread clk bool defl multitask_int xl multitask__int returns let yl yl multitask_ int defl gt pre if clk then x1 else yl jer_multitask__FastThread Condact multitask__FastThread node condact_multitask__FastThread clk bool defl multitask_int returns yl multitask_ int var x1_when_clk let xl_when_clk xl multitask__int De multitask__int when clk xl when clk yl if clk then current multitask__FastThread x1_when_clk else def1 gt pre y1 tel End of node condact_multitask__FastThread This file contains the lustre translation od AADL components as described in Section 4 The node activations and the variables releases are controlled by the scheduler variables 6 15 The model leaves to be Filled in fillme multitask_nodes lus The mo
8. inputs are considered as system outputs and their outputs are considered as system inputs In AADL it is possible to have several wires that comes into the same port The AADL standard says that the messages are queued in such a case For Data ports I don t know what it means Probably it is only allowed for event ports in AADL Anyway we reject such programs when several wires target the same data port For event port we perform a logical and between the several wires event port Boolean variable A bus is translated into a unit delay That modelisation could be refined Known limitations Only Ms are taken into account as time unit The inverse of a port group should be defined after the port group The character gt in comment kills the xml parser e g if you comment a line like Period gt 15 ms This is due to a bug in the OSATE eclipse plugin which outgh to escape the gt character i e it should generate amp gt instread of gt the xsd files directory is wrong in the aaxl cf fix_aaxl rule in examples Makefile A A quasi synchronous clock generator acceptor in Lustre V4 We give below a Lustre V4 implementation of the quasi synchronous clock generator acceptor discussed in Section 4 1 We first define intermediary nodes compute_advance computes the relative advance of ckl w r t ck2 ba_fi11 creates an array of size n filled with x ba_none checks if all elements of the arra
9. int var pc int let pe 0 gt pre c if clk2 then 0 reset the advance of ele else if ciki then pe t 1 clk got ahead of one tic else pc tel A fix priority scheduler for 3 threads node cpu_from_needs_3 qs_tick needsl needs2 needs3 bool returns cpul cpu2 cpu3 bool let cpul qs_tick and needs1 cpu2 qs_tick and needs2 and not cpul cpu3 qs_tick and needs3 and not cpul and not cpu2 tel node schedule_processorl_threads in _min_maxl in_min_max2 in_min_max3 int qs_tick bool returns _add_activate_clk _add_release_clk bool _mult_activate_clk _mult_release_clk bool _thrl_activate_clk _thrl_release_clk bool needsi needs2 needs3 bool cpul cpu2 cpu3 bool var _add_activate_clk_candidate bool _mult_activate_clk_candidate bool thrl_activate_clk_candidate bool next_needsi next_needs2 next_needs3 bool let _add activate_clk candidate timer 20 qs_tick _mult_activate_clk_candidate _add_release_clk _thrl_activate_clk_candidate timer 100 qs_tick next_needsl _add_release_clk consume in_min_maxl _add activate_clk candidate cpul needsl false gt pre next_needsl next_needs2 _mult_release_clk consume in_min max2 _mult_activate_clk_ candidate cpu2 needs2 false gt pre next_needs2 next_needs3 _thrl_release_clk consume in_min max3 _thrl_activate clk_candidate cpu3 needs3 false gt pre next_needs3 cpul cpu2 cp
10. is associated to the corresponding component For example the integer output of node incr is filtered by anode barrier_incr defined as follows Example 3 The barrier of node incr node barrier_incr clk bool y def int y int returns y_delayed int let y delayed y def gt pre if clk then y else y delayed tel The clock c1k of that barrier is computed by the node consume That node takes as input e aninteger in_min_max which may contain any value defined by the Compute_execution_time property e the activation condition trig and e the cpu variable that is true when the component have the cpu When the activation condition trig becomes true the in_min_max input is used to set the alea local variable and a counter cpt is set to 0 Then each step where cpu is true cpt is incremented When cpt becomes equal to alea the release condition is emitted i e becomes true for cycle Computing the release condition node consume in min max int trig cpu bool returns needs release bool var next_needs edge_trig bool CS 2 aime alea 3 int let alea if edge_trig then in_min_max else 0 gt pre alea needs fals gt pre next_needs next_needs dge_trig if needs then not release false else trig trig cpt if needs then if cpu then pcpt 1 else pcpt else 0 pept 0 gt pre cpt release cpu and cpt alea tel 25 When a thread i
11. 2 needs3 bool returns cpul cp u2 cpus booli let cpul tick and needsl cpu2 tick and needs2 and not cpul cpu3 tick and needs3 and not cpul and not cpu2 tel where tick is the quasi synchronous clock of the processor and needs1 resp needs2 needs3 is a boolean that indicates whether the first resp second third thread claims to be active cpul is true if the control is assigned to the first resp second third thread This scheduler can straightforwardly be generalized to n processes The variables cpul and needs1 are associated to the higher priority thread 1 e to the thread with the smallest period Note that we neglect the time necessary to perform context switch between threads but it could be taken it into account tough quite easily 4 3 Activation conditions An activation condition is added to Periodic and sporadic components processes and threads An activa tion condition is a Boolean variable that is set to true when the node needs to be activated For a component C of period p the scheduler define a Boolean variable C_act ivate_clk that is true every p cycles of the outer processor A periodic clock generator node clock_of_period period int qs_tick bool returns activate_clock bool let pept Periodi prercpt cpt if activate_clock then period els if qs_tick then pcpt 1 else pcpt activate_clock true gt pcpt 1 and qs_tick tel For example supp
12. 9 5 The aadl2sync compiler 9 Sol malaon 144 0 ee Re RA ANR SM Ra D Pine ete 9 Dr MIA br ta a A Do US Poe 9 32 1 Theaadl s nc compiler ica A A oS 9 9 2 2 Fixing the OSATE aaxl generated files acr cc ee muse eos a 11 6 Examples XXX NOT FINISHED YET 11 6 1 Two threads one processor lt osc cesede redd ue ba ew hae ee due 12 6 1 1 The scheduler schedule multitask lus 12 6 1 2 The scheduled top level node multitask lus 15 GLS Thbelucky ile muleeibesk Lue sc rer pada e dp me wee gh Ae heu Le 15 6 1 4 The translated components multitask nodes lus 17 6 1 5 The model leaves to be Filled in fillme multitask _nodes lus 17 6 1 6 A filled model fillme multitask nodes lus 18 6 1 7 Constants fillmemultitask const lus 18 6 1 8 Data types fillme multitask types lus 18 62 TWOPIOCESSOE oo LA ER ee ee eee eee eed bee ee he ee 18 7 A test session using Lurette 21 8 A formal proof session using Lesar 21 9 The currently supported AADL subset 21 9 1 IEROESA CONKERS 64 5 4 sus ae base eR ad ee st 21 92 Wotsupported concepisce i a ona ch deeds He ee A Rees 21 g3 DUPpported conces ecs g ea E SRE E Ere eS Ye Ro 22 Oe POMS desim DECISIONES os a Set e Ph Ree Hee des Bees eee des 22 93 Known limitauons 2 44 ic2 460 6 abba eee HA bbe ee eed a x 22 23 A A quasi synchronous clock generator acceptor in Lustre
13. ake body o bin aadl2sync show scheduling multitask multitask aaxl on peouvou the 29 6 2007 at 14 50 11 include fillme_multitask_nodes lus multitask__A_Process_IMPL node multitask__A_Process_IMPL _s_activate_clk bool _s_release_clk bool _f_activate_clk bool _f_release_clk bool returns 01 multitask__int 02 multitask__int var f_O_condact multitask__int f O multitask__int s_O_condact s_ 0 let fo barrier_multitask__FastThread _ multitask__FastThread_O_dft DE f_O_condact condact_multitask__FastThread _f_activate_clk s_0 multitask__FastThread_0_dft multitask__int multitask__int f_release_clk _0_condact barrier_multitask__SlowThread _s_release_clk multitask__SlowThread_O_dft s_0_condact Ve s_O_condact condact_mult itask__SlowThread _s_activate_clk _0 multitask__SlowThread_0_dft Ve s O multitask__multitask_IMPL node multitask__multitask_IMPL _s_activate_clk bool _s_release_clk bool _activate_clk bool f_release_clk bool returns slow_cmd_I multitask__int fast_cmd_I var a_process_O1 a_process_02 let fast_cmd_I a_process_02 slow_cmd_I a_process_01 a_process_01 a_process_02 _s_release_clk _f activate_clk _f_release_clk multitask__int multitask__int multitask__int multitask__A_Process_IMPL _s_activate_clk tel Barrier of multitask__SlowThread node barrier_multitask__SlowThread
14. d models of specific buses can be provided In our prototype tool we just consider buses as usual connections 25 3 3 Software components As for systems each software component except data is mapped into a Lustre node which inputs outputs 1s made of the process input output ports For process implementations the node calls result from its inner connections 3 3 1 Processes Process components are an abstraction of software responsible for scheduling and for executing threads Processes are scheduled the same way periodic threads see below the main difference being that threads executed by a process can share a common memory whereas processes executed by a processor cannot Properties When several processes run on the same processor the dispatch protocol property attached to each process is used by the scheduler to activate it It can be set to Periodic only and the period property must be set Sub components The sub components of a process can be a thread or a data Thread groups are not supported 3 3 2 Threads Thread components are an abstraction of software responsible for scheduling and for executing sub programs When several threads run under the same process the sharing of the process is managed by a runtime sched uler Properties The dispatch protocol property is used to specify the activation of a thread e periodic means that the thread must be activated according to the specified period e aperiodic mean
15. ddition oracles and quasi synchronous clocks 1 In this document we explain of the translation is performed and how the tool can be used Please refer to 4 for a complementary description of the process In the following Lustre means either the academic Lustre or Scade cf Section for a description of the various code generation options We illustrate our presentation using the academic Lustre syntax We suppose the reader in familiar with the AADL concepts cf 2 7 as well as with Lustre 3 Outline Section 2 describes the general principles of the translation and Section 3 how the translation operates component by component Section 4 describes the scheduler driving the various oracles variables introduced during the translation Section 5 presents the tool installation and usage and Section 6 illustrates its use on an example Finally Section 9 sums up which subset of AADL is supported as well as the limitations of the current version of the tool 2 The AADL to Lustre translation scheme The objective of the translation in Lustre is to be able to use the Lustre simulation and formal verification tools to validate AADL designs very early in the development process In other words we want to define in Lustre an executable formal semantics for a subset of AADL Since Lustre is a discrete time synchronous and deterministic language a synchronous and non deterministic aspects of AADL call for a particular attention From contin
16. del leaves to be Filled in node multitask__SlowThread I multitask__int returns let Ao MS tel node multitask__FastThread I multitask__ int returns let 1 2 tel O multitask__int O multitask__int When invoked with the gen fake body option the compiler put default arbitrary values to unknown entities such as undefined output variables but also to data types and constant values as illus 25 trated below One have to search for the string XXX all through the generated files in order to check whether those arbitrary values are correct 6 1 6 A filled model fi11me multitask nodes lus Here is a possible way to fill the file above node multitask__SlowThread I multitask__ int returns O multitask_ int let node multitask__FastThread I multitask__ int returns O multitask_ int let 6 1 7 Constants fillme multitask_const lus This file was generated by aadl2sync version 0 28 bin aadl2sync show scheduling vars gen fake body 0 multitask multitask aaxl2 on peouvou the 27 6 2007 at 16 54 17 const multitask__SlowThread_O_dft const multitask FastThread_0_dft ee 0 All constants are defined in this file Default values are provided when the compiler in invoked with the gen fake body option 6 1 8 Data types fillme multitask_types lus Data types This file was generated by aadl2sync vers
17. erimaG Unit Mixte de Recherche CNRS INPG UJF Verimag Manual Centre Equation 2 avenue de VIGNATE F 38610 GIERES tel 33 456 52 03 40 fax 33 456 52 03 50 http www verimag imag fr The aadl2sync User Guide Erwan Jahier Louis Mandel Nicolas Halbwachs Pascal Raymond Initial version January 12 2007 Last update January 24 2008 Software Version 0 31 Last svn checkin 2008 01 24 10 26 46 Contents 1 Introduction 2 2 The AADL to Lustre translation scheme 2 3 The AADL component to Lustre node mapping 3 Il o o ecd AS ee ee messe ee ck ee ek Aie 4 32 Hardware components s c opo menia es SE pe 4 SR RE ee 4 Bow o tt Le eee A ee a ee F 4 O o A RO Pa eRe ee be RRS 4 o WARIO ce AAA 4 DA USO Oe ce a da BIR See ds Re So ee a e 4 Sd SWA COMPONEMS 22 5 a s dere os Pk OS CAREERS SEES OEM OS 5 Al Processes toc a OR BR a ee a OER OE SRS 5 Oia PEAS Durs Lu deed SER we come we wd at eS RSS 5 sr o ENE 5 Jad DA o A A A A A de A 6 SA CNR T ON ODIS LL seu ee A EAA Eh Ee ee he ui BRAS 6 4 Modeling the AADL virtual machine 6 4 1 Qasi synchronous clocks spec ei 5S 4 ps bk OR Dee bE eS See 6 4 2 Multi tasking Time sharing 7 4 3 Activation conditions 7 Ae Release CONDITIONS ui ae a ren mm AOE et Me pape ee i 8 4 5 Formal verification versus simulation
18. f the distribution is precisely to automate this boring process 6 Examples XXX NOT FINISHED YET THIS SECTION IS NOT FINISHED YET SORRY We demonstrate in this section the use of the tool on two a bit silly examples that ougth illustrate most of the AADL features we take into account The first one is an AADL program that uses two threads of different periods that run on a single processor The second one is made of 2 processors each processor is running one process each process is running 2 periodic threads a slow and low priority thread type and fast and high priority thread implementation that runs 2 sub programs very simple exemple to illustrate what file are generated how thread are simulates 2it might be possible to say to the OSATE plugin of eclipse how to redefine that please tell me jahier imag fr if you know how 25 6 1 Two threads one processor Here is an AADL program that runs two periodic threads running on a single processor The first thread of period 16 ms returns its value betwenn 6 and 8 ms of cpu time after it has started The second thread of period 4 ms returns its value after betwenn 1 and 2 ms Each thread exchanges an integer value The top level system has no input and returns the output value of the first thread The multitask aadl file system multitask end multitask system implementation multitask IMPL subcomponents slow_cmd device An Actuator fast_cmd device
19. for that node are generated by the stochastic Lucky program of Section 6 1 3 6 1 3 The Lucky file multitask luc This Lucky program only generates values for the in min max lt i gt lt j gt variables But if the top level component had input then this program would have them in its output interface It would be up the user to define constraints over those variables The internal variables are there because the compiler has been invoked with the show scheduling vars options and because lucky imposes that the set of inputs resp outputs matches exactly the set of outputs resp inputs of the node its generates inputs for cf the Lucky manual 5 25 to be used for simulation inputs slow_cmd_I fast cema I _ amp activate cik s release clk _f activate clk _f_release_clk needs_a_processor_s needs_a_processor_f cpu_a_processor_s cpu_a_processor_f outputs INE LNE bool bool bool bool bool bool bool bool s_release_clk_min_max int f_release_clk_min_max int states loop start_state stable loop transitions loop gt loop cond 1 lt 1 lt true s_release_clk_min_max and s_release_clk_min_max f_release_clk_min_max and f_release_clk_min_max a 12 and 6 and 25 6 1 4 The translated components multitask_nodes lus The translated components This file was generated by aadl2sync version 0 28 vars gen f
20. gram this result is only available at step 21 25 6 1 2 The scheduled top level node multitask lus The scheduled top level node This file was generated by aadl2sync version 0 28 bin aadl2sync show scheduling vars gen fake body o multitask multitask aaxl on peouvou the 29 6 2007 at 14 50 11 include schedule_multitask lus include multitask_nodes lus scheduled version of node multitask__multitask_IMPL node multitask s_release_clk_min_max int f release_clk_min_max int returns slow_cmd_I multitask__ int fast_cmd_I multitask__ int we output the scheduler clocks to see what is going on cf show scheduling vars option _s_activate_clk bool _s_release_clk bool _f_activate_clk bool _f_release_clk bool needs_a_processor_s needs_a_processor_f bool cpu_a_processor_s cpu_a_processor_f bool let s_ ctivate_cik _s_release_clk f actiyate cik _f_release_clk needs_a_processor_s needs_a processor_f cpu_a processor_s cpu_a_processor_f schedule_multitask s_release_clk_min_max f_release_clk_min_max slow_cmd_I fast_cmd_I multitask__multitask_IMPL s_activate_ci1k _s_release_clk _f_activate_clk _f_release_clk This node outputs various internal scheduling variables that are there to illustrate the behavior of the scheduler Without the show scheduling vars option this node would have no output The inputs
21. ible implementation of a Quasi synchronous QS clocks generator acceptor This program is parameterized by e n the number of QS clocks to generate and e d the maximal clock drift i e the maximum number of tics that are authorized for the other clocks between 2 tics of each clock The idea is starting from a n array of Boolean values e g chosen randomly containing candidate values for the QS clocks to check that no clock drift excess occurs and to force the culprit clocks to be false when necessary to avoid this drift excess More precisely we compute the relative advance of each clock w r t the n 1 other clocks If e the relative advance of a clock c1k1 w r t another clock c1k2 is equal to d e clk1 is true e clk2 is false then we force c1k1 to be false Such a Lustre program in the V4 syntax is provided in extenso in appendix A 25 4 2 Multi tasking Time sharing Several threads that run on the same process need to share the CPU Therefore we define one scheduler per process that runs more than one thread In the current version of aadl2sync this scheduler is quite basic it is a Rate monotonic scheduler preemptive fix priority Higher priority is given to threads that have the smallest period For example in order to schedule 3 threads aadl2sync would generate the following task scheduler A rate monotonic scheduler for scheduling 3 threads node cpu_from_needs_3 tick bool needsl needs
22. ion 0 28 bin aadl2sync show scheduling vars gen fake body o multitask multitask aaxl on peouvou the 29 6 2007 at 14 50 11 type multitask__int int XXX Fix me Data types are defined in this file Here the compiler guessed it was an integer because int is a sub string of multitask__int This guess is only done if the compiler in invoked with the gen fake body option 6 2 Two processors Here is an AADL program that illustrates the translation of a model with several processors We only show the scheduler as the other generated files are very similar to the ones of the first example One can have a look a all the generated files in the examples twoproc directory of the distribution after launching the make demo command 25 The twoproc aadl file system twoproc end twoproc system implementation twoproc IMPL subcomponents tl device A Sensor t2 device A_Sensor emai l device An_Actuator email device An_Actuator cmd1_3 device An_Actuator cmd2_1 device An_Actuator cmd2_2 device An_Actuator cmd2_3 device An_Actuator processorl processor A Processor IMPh processor2 processor A_Processor IMPL processl process A Process IMPL process2 process A Process IMPL so that the 2 processes can communicate System_bus bus A_Bus memo memory Some_Memory connections bus access System_bus gt processorl proc_bus bus access System bus gt processor2 proc bus b
23. mplementation runs several sub programs those are executed in sequence The re lease condition of the a sub program is therefore plugged onto the activate condition of the following sub program The release condition of the last sub program is plugged onto the release condition of the outter thread 4 5 Formal verification versus simulation In order to perform formation verification e g model checking one should take into account that the ora cles that have been added during the translation are not completely random For example The in min max varibles ougth to be between a minimum and a maximum value This is why an additionnal node is defined in node schedule ex1 lus Oracles properties node schedule exl_oracles properties an aa ase da ima merda lia a mee S Sion aa mada mec ha mA men aia mia mens 2 8 slime aleal alea2 bool returns Ol BOOMI let ok 1 lt in min max11 and in min max11 lt 5 and 1 lt in min max12 and in min max12 lt 5 and 10 lt in min max13 and in min max13 lt 30 and 1 lt in min max21 and in min max21 lt 5 and 1 lt in min max22 and in min max22 lt 5 and 10 lt in min max23 and in min max23 lt 30 and For simulation purposes a lucky program named ex1 1uc is generated which also take those con straints into account to generate random input This generated file can serve as a basis to describe the behavior of the AADL model enviro
24. mponents 3 2 1 Devices Device components are used to interface the AADL model with its environment Therefore devices are not translated as the other components their inputs are considered as system outputs and their outputs as system inputs For simulation and verification purposes behavioral models of devices can be provided by the user Properties No property is taken into account for devices Sub components None 3 2 2 Processors Processor components are an abstraction of hardware and software responsible for executing and schedul ing processes Basically each processor will have its own clock which is the base time of the components running on the processor The Clock_period property that declares the processor internal clock rate is used in our translation to model the relations between the processors clocks More details on this scheduler are provided in Section 4 Properties The Clock period is used when the system contains several processors to generate the quasi synchronous clocks cf Section 4 1 Sub components The only possible sub component for processors are memories but those are ab stracted 3 2 3 Memory Memory components are used to specify the amount and the kind of memory that is available to other components We assume that enough memory is available and thus ignore everything that is related to such components 3 2 4 Buses Bus components are used to exchange data between hardware components Detaile
25. nd rising_edge x then true else if pre y_has_been_emitted and reinit then false else pre y_has_been_emitted tel let cpul qs_tick and needs1 cpu2 gs_tick and needs2 and not cpul tel node s dule_a_processor_threads in_min_maxl in_min_max2 int qs_tick bool returns _s_activate_clk _s_release_clk bool _f_activate_clk _f_release_clk bool needs2 bool needs1 bool cpu2 bool cpul bool var _s_activate_clk_ candidate bool _f_activate_clk_ candidate bool next_needsl next_needs2 bool let timer 15 timer 10 consume _s_activate_clk_candidate _f_activate_clk_candidate next_needs2 _s_release_clk gs ticky qs_tick in_min_maxl _s_activate_clk_candidate cpu2 next_needs1 _f_release_clk consume in_min_max2 _f_activate_clk_ candidate cpul needs1 false gt pre next_needs1 needs2 false gt pre next_needs2 cpul cpu2 cpu_from_needs_2 qs_tick needsl needs2 We read inputs when the thread starts having the cpu not needs2 not needs1 _s activate_clk first_rising_edge cpu2 _f activate_clk tel node schedule_multitask _s_release_clk_min_max int f_release_clk_min_max int first_rising_edge cpul returns _s_activate_clk bool _s_release_clk bool _f_activate_clk bool f_release_clk bool rr tr _ _ _ _ _ _ __ _ int activate bool bool node consume returns var needs cpt pc
26. ne such tool is developed within the ASSERT project Each data subcomponent is translated into a local variable of the containing component If the contain ing component provides an access to that data then its interface is modified e read_only one output is added e write only one input is added e read write one output and one input are added e by method the interface remains unchanged 3 4 Other concepts AADL defines a concept of operational mode that is ignored in the current version of the tool A concept of Flow is also introduced to allow users to declare the existence of logical flows of information between a sequence of components Flows are used to perform various non functional analysis Therefore they are ignored in our translation too 4 Modeling the AADL virtual machine In order to model non determinism oracles are added to node inputs Each node carries all the oracles necessary to control its sub nodes The top level node therefore potentially have quite a lot of such oracles two per component leave instances one for the activation condition and one for the release condition plus as many quasi synchronous clocks as there are processors All those oracles are controlled by a centralized scheduler that is automatically generated This scheduler models the behavior of the AADL virtual machine We describe below what this generated scheduler looks like 4 1 Quasi synchronous clocks We describe in this Section a poss
27. nment to generate realistic input sequences 5 The aadl2sync compiler 5 1 Installation aadl2sync is a stand alone executable Therefore one just needs to put it somewhere accessible via the PATH environment variable The environment variable AADL_SCHEMA_DIR ought to be set to a directory containing the aaxl schema definitions Those can be found on the OSATE website or in the aadl schema directory of the aadl2sync distribution The Makefile in the example directory assumes that the Lurette tools are accessible from the PATH This tool suite can be downloaded there http www verimag imag fr synchron index php page lurette download 5 2 Usage 5 2 1 The aadl2sync compiler Actually aadl2sync does not take as input aadl files but their aaxl counter parts Those can be obtained via the Eclipse plugin of OSATE If you edit your AADL programs with an external editor emacs vi etc 25 one just needs to open the AADL file with the Eclipse OSATE editor and the aaxl files are automatically generated If one launches the aadl2sync compiler using the h option one gets This is aadl2sync version 0 30 Usage aadl2sync lt options gt lt file gt aaxl lt options gt are output file lt str gt o lt str gt output file base name lustre Generate academic lustre code for the Verimag compiler the default scade Generate lustre code that is compatible with Scade verbosity level lt int gt
28. nt Type describes the functional interface of the component An Implementation inherits of the corresponding component Type attributes It also declares the sub components it is made of as well as the connections between them Those connections are made through the sub components input and output ports An AADL model is made of an arborescent assembly of software and hardware component types or implementations A system is made of several devices and processors each processor can run several 25 processes each process can run several threads and each thread can run several subprograms Leaves of the AADL model are therefore either subprograms or component types We need actual Lustre code for those leaves to be able to perform formal verifications and simulations 3 1 Systems A system is the top level component of the AADL model It is translated into a top level Lustre node Each input resp output port of the system is mapped into an input resp output of the node For system implementations each sub component is mapped into a Lustre node obtained by the translation The node calls result straightforwardly from its inner connections Properties No property is taken into account for systems Sub components The sub components of a system can be processors processes devices and data It can also be memory and bus but those are abstracted away by the tool It could also be systems but this is not supported yet 3 2 Hardware co
29. odel The bodies of such nodes need to be provided e fillme ex1_const lus that contains various constants that needs to be defined such as the components initial values i e the values they ought to output at the first cycle values that are used to provide default values in activation conditions e fillme exl_ types lus that contains the Lustre type definitions of Data type components This translation is not automated by aadl2sync but external tools exist that translate asn1 type definition to Lustre for example Those last 3 files which are prefixed by i11me need to be filled in and renamed without the prefix If aadl2sync is launched with the gen fake body option fake values are provided for each of the entity to be defined The content of those 6 files is illustrated and described further in Section 6 5 2 2 Fixing the OSATE aaxl generated files As any xml document aaxl files ought to define in their header second tag the URI where to find the xml schema they are supposed to conform to However the aaxl files generated by OSATE defines to a wrong URI http AADL In order to turn around this problem aadl2syne copies those schema files in the tmp aadl schema directory using the AADL_SCHEMA_DIR environment vari able Therefore one just needs to fix the aaxl file e g with sed so that it points to this directory The purpose of the fix_aax1 rule of the Makefile provided in the examples directory o
30. ose that we have an AADL model leaf which is a periodic thread type and which corresponds to the Lustre node incr that increments an integer Example 1 A Lustre node that increments a integer node incr x int returns y int let y x 1 The components that call this thread would not call incr directly but would call condact_incr 25 Example 2 The condact of node incr node condact incr clk boo1 y def int x int returns y int let y if clk then current incr x when clk else y def gt pre y The node condact_incr has 2 additional inputs A Boolean c1k that is used to activate the the node incr when c1k is true the node incr is called and otherwise the node incr outputs the value stored in amemory computed the last time the node was activated The second additional input y_def is used to be able to provide an initial value to the memory In Scade there exists a cond_act operator that do exactly the same thing Therefore when generating Scade code we generate cond act incr clk y def x instead of condact_incr clk y def x and we do not need to define condact_incr at all 4 4 Release conditions In the synchronous framework nodes compute outputs from inputs instantaneously In order to simulate that subprograms and threads do take time we simply add barriers that retain the output values a certain amount of cycles That number of cycles is determined by the Comput e_Execut ion_t ime property that
31. pt alea int let nemin mag cpu n xt_nbbas tdr edge_activate bool int in_min alea ax is ignored except when activate becomes true if edge_activate then in_min_max else 0 gt pre alea false gt pre next_needs edge_activate needs next_needs if needs then not term false else activate activate cpt if needs then if cpu then pcpt 1 else pcpt else 0 pcpt 0 gt pre cpt term cpu and cpt alea cpull cpul2 bool 25 let _s_activate_clk _s_release_clk _f_activate_clk _f_release_clk needs11 needs12 cpull cpul2 schedule_a_processor_ _s_release_clk_min_max _f_release_clk_min_max true Ya reads 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 slow_cmd_1 fast_cmd_1 S_activate_clk _s_release_clk _f_activate_clk f_release_clk needs_a_processor_s needs_a_processor_f cpu_a_processor_s cpu_a_processor_f Figure 3 Another timing diagram obtained from a simulation of multitask aadl the second activation of the fast thread was able to read the result of the slow thread at step 7 whereas in previous dia
32. pu _add activate_clk_2 first_rising_edge cpul not needs1 _mult_activate_clk_2 first_rising_edge cpu2 not needs2 _thrl_activate_clk_2 first_rising_edge cpu3 not needs3 tel A quasi synchronous scheduler for 2 processors node quasi_synchronous_scheduler alea_1 alea_2 bool returns qs_1 qs_2 bool var advance_max_is_reached_1_2 bool advance_max_is_reached_2_1 bool problems_1_2 bool problems_2_1 bool filter_1 bool filter_2 bool advance_1_2 int advance_2_1 int padvance_1_2 in padvance_2_1 int let We compute the relative advance of various processors advance_1_2 compute_advance qs_1 qs_2 advance_2_1 compute_advance qs_2 qs_1 padvance_1_2 0 gt pre advance_1_2 padvance_2_1 0 gt pre advance_2 Is the maximum advance reached advance_max_is_reached_1_2 padvance_1_2 gt 2 advance_max_is_reached_2_1 padvance_2_1 gt 2 there is a problem if the maximum advance is reached and no tic occurs problems_1_2 advance_max_is_reached_1_2 and alea_1 problems_2_1 advance_max_is_reached_2_1 and alea_2 we force the tic for clocks chat are d tics late filter_1 not problems_1_2 filter_2 not problems_2_1 and true qs_1 alea_1 and filter_1 qs_2 alea_2 and filter_2 tel node schedule_twoproc in_min_maxll in_min_max12 in_min_max13 int in_min_max21 in_min_max22 in_min_max23 int aleal alea2 bool return
33. pute_Execution_Time gt 10 ms 30 ms end Threadl thread Thread2 features 11 in data port int I2 in data port int O1 out data port int 02 out data port int properties Dispatch_Protocol gt Periodic Period gt 20 ms end Thread2 thread implementation Thread2 IMPL calls add subprogram ADD mult subprogram MULT Foo connections parameter 11 gt add 11 parameter 12 gt add 12 parameter 11 gt mult 11 parameter 12 gt mult 12 parameter add O gt O1 parameter mult O gt 02 end Thread2 IMPL subprogram ADD features Il in parameter int 12 in parameter int O out parameter int properties Compute_Execution Time gt 1 ms 5 ms end ADD subprogram MULT features il in parameter int i2 in parameter int O out parameter int properties Compute_Execution_Time gt 1 ms 5 ms end MULT 25 The scheduler This file was generated by aadl2sync version 0 27 bin aadl2sync show scheduling vars gen fake body o twoproc twoproc aaxl on peouvou the 12 6 2007 at 11 19 31 include fillme_twoproc_types lus include fillme twoproc_const lus We skip definitions provided in the previous example timer definition skipped rising edge definition skipped first_rising edge definition skipped consume definition skipped Compute the relative advance of clkl w r t clk2 node compute_advance c1k1 clk2 bool returns c
34. r cases the non determinism is stated explicitly For example a thread or a sub program may have the property that its compute execution time ranges from 10 to 100 Ms In such a case we add a boolean input that controls whether to retain the previous value of the component or to deliver a new value This oracle has the property to be true between 10 and 100 cycles after the thread is activated In the following we call oracles that control the cycle at which the components output values are available release conditions Modeling a synchronous components Programs that try to exchange values run on different processors migth be sensible to clock drift One way to weaken the synchronous hypothesis to model a synchronous components is to use quasi synchronous clocks 1 Clocks are said to be quasi synchronous resp n quasi synchronous if between two successive activations of one clock the other clocks are activated at most twice resp n times Such an interleaving is illustrated in Figure 1 The figure pictures the timing diagram of two quasi synchronous clocks ck1 and ck2 The relative advance of ck1 over ck2 a1 and of ck2 over ck1 a2 are represented for clarifying the principle whenever c1 resp c2 is true a2 resp al is reset meanwhile if c2 resp c1 is false al resp a2 is incremented Since in the example al and a2 are both bounded by 2 the clocks are so far quasi synchronous al 0 0 0 1 2 0 0 0 1 0 0 1 I
35. s _add_activate_clk bool _add_activate_clk_2 bool _add_release_clk bool _add_release_clk_2 bool _mult_activate_clk bool _mult_activate_clk_2 bool _mult_release_clk bool _mult_release_clk_2 bool _thrl_activate_clk bool _thrl_activate_clk_2 bool _thrl_release_clk bool _thrl_release_clk_2 bool qs ticki qs_tick2 bool needs11 needs12 needs13 bool cpull cpul2 cpul3 bool needs21 needs22 needs23 cpu2l cpu22 cpu23 bool let bool _add_activate_clk _add_release_clk _mult_activate_clk _mult_release_clk _thrl_activate_clk _thrl_release_clk needs11 needs12 needs13 cpull cpul2 cpul3 schedule_processorl_threads in_min_maxll in_min_max12 in_min_max13 as_tickl _add_activate_clk_2 _add_release_clk_2 _mult_activate_clk_2 _mult_release_clk_2 _thrl_activate_clk_2 _thrl_release_clk_2 needs21 needs22 needs23 cpu2l cpu22 cpu23 schedule _processor2_threads in_min_max21 in_min_max22 in min_max23 qs_tick2 qs_tickl qs_tick2 quasi_synchronous_scheduler aleal alea2 tel 0 be used for formal verification node schedule_twoproc_oracles_properties in_min_maxll in_min_max12 in_min_max13 int in_min_max21 in_min_max22 in_min_max23 int aleal alea2 bool returns ok bool let 1 lt in_min_maxll and in_min_maxll lt 5 and 1 lt in_min_maxl2 and in_min_max12 lt 5 and 10 lt in_min_max13 and in_min_max13 lt
36. s that the thread is activated via one of the other components output port called an event port e a sporadic thread is a mixture between aperiodic and periodic it can be activated either by events or periodically e background threads are always active but have the lowest priority The property compute exec_time is necessary for thread Types so that the scheduler knows when to make the outputs available For thread implementations this execution time results from the compute_exec_t ime associated to their sub programs Sub components Thread implementations are made of sub program calls and data 3 3 3 Sub programs Sub program components represent elementary pieces of code that processes inputs to produce outputs Only their interfaces are given in the AADL model sub program implementations ought to be provided in some host language For our purpose we require sub programs to be given in a synchronous language Scade or Lustre Moreover sub programs must be provided with a compute_exec_t ime property in order to simulate accurately the time their computations take Properties A sub program must define a compute_exec_time property so that the scheduler knows when to release its outputs Sub components None 25 3 3 4 Data Data components are not associated to Lustre nodes but to Lustre types They are not handled by aadl2syne except for the base types bool int and floats and must be set by users or a third party tool o
37. tially in future versions of the tool 9 2 Not supported concepts The following concepts could prevent the translation to occur if used in the AADL model e port groups mixing input and output ports in out e systems as sub component of systems thread groups e modes e sporadic aperiodic and background threads execution fault handling in threads fi e event ports since event data ports are used to trigger non periodoc thread or or to cause a mode switch it would be meaningless to take them into account yet t e subprograms as features remote procedure calls e subcomponent accesses outside their containment hierarchy All those concepts could be supported by the tool one day 25 9 3 Supported concepts The translation of those concepts was described in Section We simply recall them here for the sake of completeness 9 4 9 5 25 systems devices processes periodic and sporadic threads sub programs sub programs calls sub program parameters data ports and port groups some properties compute exec time an interval associated to threads and subprograms Period associated to processes and threads dispatch protocol which must be equal to Periodic or Sporadic Some design decisions If a component implementation exists no node is generated for the corresponding component Type Devices are not translated into a Lustre node as other components instead their
38. tics whereas thr2_activate is not always true every 10 tics It is because a thread is activated after period tics as soon as it has the cpu And since thr2 is not the most prioritary thread sometimes it is activated a little bit later than its period i e once thr1 release the CPU Here are the files generated by aadl2sync to obtain that simulation are described in the sequel 6 1 1 The scheduler schedule multitask lus The file named schedule multitask lus defines the node schedule multitask that schedules the top level system The inputs named in min_max_ lt i gt lt 3 gt are used to simulate the compute execution time of the two threads lt i gt refers to the processor number and lt j gt refers to the thread number of pro cessor i Their values are set by the generated program Lucky file multitask luc 6 1 3 described below This node outputs the various scheduling variables that indicate when a thread is activated _thr lt j gt _activate_clk when its output should be made available to other components _ thr lt j gt _release_clk need lt i gt lt j gt is true when the 7th thread of the th processor ask for the CPU cpu lt i gt lt 3 gt is true when the jth thread of the th processor has the CPU 25 10 20 24 27 28 31 35 36 40 slow_cmd_I fast_cmd_I S_activate_clk _s_release_clk _f_activate_clk f_release_clk needs_a_processor_s
39. u3 cpu_from_needs_3 qs_tick needsl needs2 needs3 We read inputs when the thread starts having the cpu _add_activate_clk first_rising_edge cpul not needs1 _mult_activate_clk first_rising_edge cpu2 not needs2 _thrl_activate_clk first_rising_edge cpu3 not needs3 tel node schedule_processor2_threads in _min_maxl in_min_max2 in_min_max3 int qs_tick bool returns _add_activate_clk_2 _add_release_clk_2 bool _mult_activate_clk_2 _mult_release_clk_2 bool _thrl_activate_clk_2 _thrl_release_clk_2 bool needsi needs2 needs3 bool cpul cpu2 cpu3 bool var _add_activate_clk_2 candidate bool _mult_activate_clk_2_candidate bool _thrl_activate_clk_2 candidate bool next_needsi next_needs2 next_needs3 bool let _add_activate_clk_2 candidate timer 20 qs_tick _mult_activate_clk_2_candidate _add_release_clk_2 _thrl_activate_clk_2 candidate timer 100 qs_tick next_needsl _add_release_clk_2 consume in_min_maxl _add_activate clk 2 candidate cpul needsl false gt pre next_needs1 next_needs2 _mult_release_clk_2 consume in_min max2 _mult_activate_clk_2 candidate cpu2 needs2 false gt pre next_needs2 next_needs3 _thrl_release_clk_2 consume in_min max3 _thrl_activate_clk_2 candidate cpu3 needs3 false gt pre next_needs3 cpul cpu2 cpu3 cpu_from_needs_3 qs_tick needsl needs2 needs3 We read inputs when the thread starts having the c
40. uous to discrete time It is not really specified in the AADL model if the time is continuous or discrete but what is certain is that for Lustre the time is discrete In order to discretize the time we map the basic clock to the smallest time units that appears in the AADL model For example if the smallest time units that is used in the model are the milli seconds Ms then the basic clock will be rated at 1 milli second Modeling implicit non determinism The first source of non determinism in AADL comes from the fact that when defining a set of programs threads processes running on different processors the time clocks when every components is activated or deliver its output is left unspecified In order to model uncertainty in Lustre a classical solution is to introduce oracles an oracle is a Boolean variable that is added to the program inputs For example here we can add a Boolean input that is true when the thread ought to be activated As it is an input formal verification tools e g model checkers would verify that the properties one wants to check holds for all the possible values of that oracle Note however that oracles are generally not completely free variables they respect some constraints such as for example that 2 threads can not run 25 together on the same process In the following we call oracles that control the activation of components activation conditions Modeling non instantaneous executions In some othe
41. us access System bus gt memo mem data port process1 01 gt cmdl_1 data port process1 02 gt cmdl_2 data port process1 03 gt cmdl_3 data port process2 01 gt cmd2_1 data port process O2 gt cmd2 2 data port process2 03 gt cmd2_3 data port t1 0 process1 1 data port tO gt Processa T HHHHHH properties Actual _ Processor Binding gt reference processor1 applies to process1 Actual_Processor_Binding gt reference processor2 applies to process2 end twoproc IMPL device A_Sensor features O out data port int end A_Sensor device An_Actuator features I in data port int end An_Actuator memory Some_Memory features mem requires bus access A Bus end Some_Memory processor A_Processor features proc_bus requires bus access A Bus end A_Processor processor implementation A_Processor IMPL end A_Processor IMPL process A_Process features I in data port int O1 out data port int 02 out data port int 03 out data port int end A_Process process implementation A_Process IMPL subcomponents EREL thread Threadl ERES thread Thread2 IMPL connections data port I gt thri E data port I thr2 i data port thls ONS Che 2 12 data port thri gt 01 data port thra 0l gt 02 data port thr2 02 gt 03 end A_Process IMPL thread Thread1 features I in data port int O out data port int properties Dispatch_Protocol gt Periodic Period gt 100 ms Com
42. vance_max_is_reached and not alea n we force the tic for clocks that would be more than d tics late filter ba_none n n problems select alea and filter advance compute_advance ba_fi1l1l n n select select n padvance 0 n n gt pre advance tel That program can be used to perform formal verification e g model checking of the corresponding AADL model In order to be able to perform simulations the only thing that remains to be done is to generate arrays of random values Note that this program is used if aadl2sync is launched with the v4 arrays options Otherwise it is an array expanded version of it less readable that is generated References 1 P Caspi C Mazuet and N Reynaud Paligot About the design of distributed control systems the quasi synchronous approach In SAFECOMP 01 LNCS 2187 2001 1 2 25 2 P H Feiler D P Gluch J J Hudak and B A Lewis Embedded system architecture analysis using SAE AADL Technical note cmu sei 2004 tn 005 Carnegie Mellon University 2004 1 3 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 1 4 N Halbwachs and L Mandel Simulation and verification of asynchronous systems by means of a synchronous model In Sixth International Conference on Application of Concurrency to System Design ACSD 2006 Turku Finland June 2006 1
43. y lt int gt Set the verbosity level gen fake body Generate a fake body to bodyless nodes toplevel system C Set the top level system one of the system is used if left unset gen random func Generates random functions instead of adding oracle variables as node inputs one file Generates only one file instead of 6 v4 arrays Use Lustre V4 arrays in the generated cod check schedulability Add an additional boolean output schedul_ok that is true as long as no dead l show scheduling vars Add the internal scheduling variable at node outputs for debugging or and to understand what s going on version version Show the version help help H Display this help message Tt ought to be possible to call this aadl2aaxl translator outside from Eclipse if anyone knows how to do it please let me know 25 For instance the command line call aad12sync ex1l aaxl would generate 6 files e exl lus that contains the top level nodes ex1_simu and ex1_verif that can be respectively used for for simulation and formal verification It also includes the other files described below e exl_nodes lus that contains the translation in Lustre of all AADL components present in the model e ex1_scheduler lus that contains the scheduler driving all the oracles introduced during the translation e fillme_exl_nodes 1lus that contains the interface of nodes corresponding to leaves in the AADL m
44. y are false qs is main node of the quasi synchronous scheduler for processors with the same clock rate It is paramaterized by e nis the number of clocks to generate e dis the maximal authorized clock drift i e the maximum number of tics authorized for the other clocks between 2 tics of each clock e alea is an array of random values n clock candidate values e select is the same alea except for clocks that are d tics late that are forced to false 25 A quasi synchronous clock generator acceptor in Lustre V4 Compute the relative advance of clk1 w r t clk2 node compute_advance c1k1 clk2 bool returns c int VAT pe Int let pe WO S joe ep if elk2 then 0 reset the advance of clki else te clk then pe cli gon ahead or one CIC else pc tel Create an array of size n filled with x node ba_fi11 const n int x bool returns t bool n let t Scene Check if all elements of the array are false node ba_none const n int I bool n returns ok bool var Now bool ni let Noe moe LOI NS OPS ancl not Lie si Ne ok Nor n 1 tel node gs const n int const d int alea bool n returns select bool n var advance_max_is_reached problems bool n n aie 2 Noel ime advance padvance int n n let advance_max_is_reached padvance gt d n n there is a problem if the max advance is reached and no tic occurs problems ad
Download Pdf Manuals
Related Search