Polychrony SSME User Guide
Contents
1. 13 4 5 3 Applying Polychrony SEIVICES ccisicecstesospacenncnadonennasendsadtacckerebeuidaddaditamuamemwndy 15 4 5 4 aN AMO emet HR 18 ASALT CIC Fe cH 18 494 2 JAVA irigi ironia a a a nas tenes eT 18 Index of Illustrations 04 26 2012 Polych rony Polychrony_SSME_UserGuide Page 3 19 1 Preface 1 1 Table of versions Version Date Description amp rationale of Sections modified modifications 1 2 Table of references and applicable documents Reference Title amp edition Author or editor Year 1 3 Acronyms and glossary Term Description SSME Signal Syntax Model under Eclipse 04 26 2012 Polych rony Polychrony_SSME_UserGuide Page 4 19 2 Subject 2 1 Purpose of the document This document is a user manual for the SSME Platform a component of the Polychrony Toolset It is a front end to the Signal ToolBox in the Eclipse environment 2 2 Editing particularities 2 2 1 Changes identification All the changes made since the previous publication are identified using the sign in the left margin of each line holding a modification 2 2 2 Temporary editing Special points are signaled like this temporary incomplete to be defined to be confirmed 2 3 Application scope 2 4 Edition and evolution of the document Tell here who is responsible of the evolution of the document and w2. init Vm e Booleans to events It rewrites boolean expressions of under sampling for logical and relational operators the goal is to prove synchronization constraints of the system o the rewriting of the booleans expressions referenced in an extraction when E when E is not a free condition and not declared as an assumption For example the expression when A and B is equal to the clock intersection of 04 26 2012 Polych ro ny Polychrony SSME UserGuide Page 9 19 when A and when B So classical boolean rules completed with some specific rules induced by the extraction and merging Signal operators are applied to the system o the rewriting of the boolean expressions referenced in the extraction when E when E is assumed to be an assertion the expression assert E specifies that E is always true when it is available So it induces that when E is equivalent to the clock of E e Signal unifications this operation consists in the merge of nodes into one node when their definition expression are equal syntactically e Clock calculus it performs the resolution of the clock systems using a triangularization technique A BDD based data structure is used Here only the study of static properties is performed They allow to characterized the set of states in which the automaton associated to a program can evolve independently of initial values and the set of the transitions between these states The result is a forest o
3. System Library jre1 6 0_07 Copy Ctrl C BA Referenced Libraries B Copy Qualified Name amp SignalGraphicalJavaStd jar pss oiu amp SignalJavaStd jar Sue t Delete Delete Build Path id Source Alt Shift S gt Refactor Alt Shift T gt Import e Export f Refresh F5 Close Project Close Unrelated Projects Assign Working Sets E 1 Java Applet Alt Shift X A 04 26 2012
4. of compilation scenarios for a Polychrony model A compilation scenario is composed of different kinds of functionalities and generators A functionality modifies the internal representation of the program a generator translates this representation into a specific external format The meta model of this plug in is shown on the next picture lt lt enumeration gt gt GeneratorKind Signal Signal LIS Signal TRA Ssme SignalAbstraction Sigali C ANSI all Fal 3 a java Profiling Lustre Syndex Polychrony SSME UserGuide H Scenario description EString c displayWarnings EBoolean elements 1 uL B Scenarioltem Page 8 19 enumeration FunctionalityKind Retiming Boolean2Events SignalUnifications ClockCalculus Events2 Boolean Abstraction Clustering Sequentializing Flattening EH Functionality H Generator gt kind GeneratorKind gt kind FunctionalityKind 4 3 1 Functionalities The functionalities that can be applied are those of the Polychrony Signal ToolBox For the moment the following functionalities can be applied to a program e Retiming It performs a shift register transformation It rewrites synchronous function f such that Y f X1 m1 init V1 Xn mn init Vm into Y y j init f V1 Vm and y f X1 m1 init V1 Xm mn
5. sig file e Signal Textual LIS it translates the internal representation of the specification 04 26 2012 Polych ro ny Polychrony SSME UserGuide Page 10 19 into a textual Signal file sig file after the graph creation The errors will be written on the file Signal Textual TRA it translates the internal representation of the specification into a textual Signal file sig file after the clock calculus phase Signal Model Ssme it translates the internal representation of the specification into a XMI Model Signal file ssme file This model file is conformed to the SSME meta model Signal Abstraction it translates the abstraction of the internal representation into a textual Signal file sig file Sigali it translates the internal representation of the specification into a textual Sigali file 23z file This file is then used by Sigali to prove dynamical properties C ANSI it translates the internal representation of the specification into a textual C ANSI files c and h files These files are used to simulate the Signal specification It is applied to a graph which must be a sbDC one The graph is with or without clusters C it translates the internal representation of the specification into a textual C files cpp and h files These files are used to simulate the Signal specification It is applied to a graph which must be a sbDC one The graph is with or without clusters Java it translates the
6. 64 efr irisa espresso ssme polychrony gtk linux x86 lib for Linux x86 efr irisa espresso ssme polychrony gtk linux x86 64 lib for Linux x86 64 efr irisa espresso ssme polychrony cocoa macosx x86 lib for MacOS X Intel x86 efr irisa espresso ssme polychrony cocoa macosx x86 64 lib for MacOS X intel x86 64 Currently there is not automatic generation of makefile to compile C C file 4 5 4 2 Java For the Java generation code we take benefit of Eclipse which is originally a Java environment which provides several facilities to manage Java project The call of the Java generation code creates if all previous operations are executed without errors a Java project containing the Polychrony Java libraries SignalJavaStd jar and SignalGraphicalJavaStd jar and the Java source classes are generated in the src directory of the project There may be some errors in the Java code if your SSME model has constant parameters The correction of these errors consists in replacing the UNDEFY calls by the value of the constant parameter To execute the simulation you have only to right click on the project or on the Java class corresponding to the main and select Run As gt Java Application 04 26 2012 Polych ro ny Polychrony SSME UserGuide Page 19 19 35 Watchdog B src Mew gt 8 default package Go Into E D Watchdog_externalsProc j ni Open in New Window D Watchdog io java P amp 4n Watchdog java HBA IRE
7. Polych rony Polychrony_SSME_UserGuide Page 1 19 POLYCHRONY A TOOLSET FOR SIGNAL SSME Platform Polychrony SSME User Guide VO Author s Checked by Approbation Name Members of the Loic Besnard Jean Pierre Talpin Espresso Team Thierry Gautier Paul Le Guernic Company INRIA INRIA CNRS INRIA Department Espresso Team Espresso Team Espresso Team Date Visa Summary User Guide of the Polychrony SSME a front end to the Signal ToolBox in the Eclipse environment Attention la responsabilit des entreprises et des organismes ayant particip l laboration de ce document ne peut en aucun cas tre engag e en cas de dommages ou de pertes r sultant de l utilisation ou de l exploitation des informations qui y sont contenues Disclaimer Contractors participating to this report shall incur no liability whatsoever for any damage or loss which may result from the use or exploitation of information and or Rights contained in this report 04 26 2012 Polych rony Polychrony_SSME_UserGuide Page 2 19 Table of Contents TDPRI A CS Me Y O Y 3 1 1 Table Of VElSlONSrescuicnreessmsmesacneraneseshnanectadememeseamanennndamenesesmibanundimensees DROXE SEQUAMUR SEN EAE 3 1 2 Table of references and applicable documents eeeeeereeeeeeee 3 1 3 Acronyms and GQlOSSANY vatcsnccereedsvereionmtmentace
8. ce For example here the Double declaration of A error is linked with the highlighted Identifier A 4 5 2 Compiler configuration The Signal compiler can be parameterized to specify the memory size used for its Operations To access to these parameters select the Polychrony section in the Preferences Window as shown in the following picture type filter text P General b Ant b C C b Help b Install Update P Java b Run Debug gt Team b Topcased P Ecore Tools Diagram OSATE Preferences P Plug in Development Maximum number of entry in the type table only updated after reboot Polychrony Memory size in bytes for the internal tree structure only updated after reboot amp Polychrony General settings for the Polychrony SSME editors Search paths for Polychrony libraries local Eclipse workspace ssmejfr irisa espresso ssme polychrony gtk linux x86 64 lib Std Memory size in bytes for the string structure only updated after reboot a x Pry Dry v New Remove Up Down 60000000 1048575 Restore Defaults Apply men J oe 04 26 2012 Polych rony Polychrony_SSME_UserGuide Page 14 19 There are four parameters e The Polychrony library path Here you add all paths in which there are LIB or SIG file that contain the Signal module needed for the compilation A lib directory that contains all libraries provided with the classical Polychrony environme
9. ces right click on the SSME file on which you want to apply the service s and select Polychrony You can choose to use a predefined scenario in this case select the Execute Predefined Scenarios option Seven actions are proposed e Generate C files from the selected SSME model Generate C files from the selected SSME model Generate Java files from the selected SSME model Generate SIG file from the selected SSME model Generate SIG LIS file from the selected SSME model Generate SIG TRA file from the selected SSME model Execute a compilation scenario on the model The three first actions generate the executable code files respectively in C C Java language from the SSME model specifications The next three actions generate a Signal textual file a normal SIG file a pretty printing of the tree internal structure or a Signal file generated during the transformation to the internal graph structure The last option applies a compilation scenario on the SSME model see previous part All these files are generated only in a directory named as the SSME model file They are only generated if all previous compilation steps are all successful It is also possible to call Polychrony services on SIG file Right click on the SIG file and select Polychrony to obtain all actions proposed for the SSME file and one action to generate a SSME file from the SIG file in a directory named as the SIG file 04 26 2012 Polych ro ny Polychrony SSME Us
10. cesses for instance an unsafe car driver Using Signal allows to specify an application to design an architecture to refine detailed components down to RTOS or hardware description The Signal model supports a design methodology which goes from specification to implementation from abstraction to concretization from synchrony to asynchrony The principal application areas for the Signal language are that of embedded real time critical systems Typical domains include e Process control e Signal processing systems e Avionics e Automotive control e Vehicle control systems e Nuclear power control systems e Defense systems e Radar systems It constitutes a development environment for critical systems from abstract specification until deployment on distributed systems It relies on the application of formal methods allowed by the representation of a system at the different steps of its development in the Signal polychronous semantic model For more information concerning the INRIA Polychrony environment consult the ESPRESSO team website http www irisa fr espresso Polychrony The POLYCHRONY TOOLSET See Illustration 1 contains three main components The Signal ToolBox a batch compiler for the SIGNAL language and a structured API that provides a set of program transformations The Signal ToolBox can be installed without the other components The Signal GUI a Graphical User Interface to the Signal ToolBox edi
11. erGuide Page 16 19 There are two more options the interactive compilation and the general compilation Let s see the interactive compilation first to be able to use it choose the General Compilation menu in the Polychrony menu and then click on Interactive Compilation A new window will pop up with all the options available in the scenario editor LJ Interactive Compilation 3x General Options Signals Unification Flattening Clock Calculus Sequentializing Retiming Booleans To Events Abstraction Sequential Clustering Profiling Export Tools Lustre Generation Syndex Generation Z 3Z Sigali Code Generation C Generation C Generation Java Generation Signal Forms Signal Generation Signal LIS Generation Signal TRA Generation Signal Abstraction SSME Generation Quit Each time you click on an option the corresponding operation is realized in real time When you have finished you can close this window by clicking on the Quit button 04 26 2012 Polych rony Polychrony_SSME_UserGuide Page 17 19 To use the general compilation GUI choose the General Compilation menu in the Polychrony menu and then click on General Compilation A GUI with tabs will pop up General Compilation General Options Partitioning Export Tools Code Generation SIGNAL Forms Miscellaneous C Generation C Generation O Java Gen
12. eration Compile Quit Check Delay Multiplexing O Force Delay Optimizing O Distribution Each time you re clicking or unclicking an option the option manager of the SIGNAL compiler is called and the corresponding options are activated or unactivated The compilation starts when you push the Compile button 04 26 2012 Polych rony Polychrony_SSME_UserGuide Page 18 19 4 5 4 Simulation The Polychrony services provides several kinds of generators which needs external tools to be used or executed SynDEx tools for sdx files Sigali distributed with the classical Polychrony distribution for z3z files The C C or Java code generation is dedicated to simulations By default the code C C or Java generated by Polychrony will read input values from a files called R input name gt dat or RC input name gt dat if the input signal is of type event and will write output values into a file called W output name gt dat These input files has to be created and filled by the user one value per line and for event signal O for absence and 1 for presence 4 5 4 1 C C For C and C you will need to use an external C C compiler The Polychrony libraries are provided and can be found in the Eclipse plugins directory and specifically in efr irisa espresso ssme polychrony win32 win32 x86 lib for Windows x86 efr irisa espresso ssme polychrony win32 win32 x86 64 lib for Windows x86
13. f clock trees e Events to booleans it performs the inter format DC that constrains event objects forest of trees of clocks to bDC without event objects a tree of boolean clock translation e Abstraction it computes the abstraction of the program I O data dependences I O clock relations the black Box or the grey Box abstraction representation This abstraction is useful for separated compiling e Sequential clustering it performs the following partitioning called input train Two nodes are in the same set if and only if they depends on the same subset of inputs signals of the graph The graph is modified The nodes are clustered into sub graphs The internal representation must be in bDC sub format e Sequentializing it performs the inter format bDC a tree of boolean clocks to sbDC sequentialized boolean dc translation The internal representation must be in bDC sub format The nodes of the internal representation are ordered The assert nodes are visible for code generation code will be generated for verifying assumptions at run time e Flattening STS it performs the inter format bDC a tree of boolean clocks to STS a tree of boolean clocks reduces to one level translation The internal representation must be in bDC sub format 4 3 2 Generators There are 12 kinds of generators e Signal Textual SIG it translates the internal representation of the specification into a textual Signal file
14. he creation of anew SSME model file the reflexive editor has a wizard To start the wizard right click on the project where you want to create your model and select New gt Other and then select the following model file SSME gt SSME Model o X Select a wizard gt Wizards type filter text Tiles gt Java Emitter Templates b Plug in Development ij SSME Compilation Model A SSME Model b amp SVN gt Topcased gt User Assistance ima J Once you have selected the SSME Model the SSME wizard is opened Then you have to choose the name of the diagram Select Next and then select the kind of the root for the model file There are three kinds of root model elements e List Module it corresponds to a library of components types and constants e Process Model it corresponds to a SIGNAL component process node action function e Operator Model it corresponds to a SIGNAL operator definition Once you have chosen the root model you only have to add new model objects To do so right click on the node on which you want to add a child and select the New Child 04 26 2012 Polychrony menu It displays the list of all possible model elements that can be added for the current selected element If this option does not exist for a node it means that there is no possible child for this node 4 3 The compilation scenarios This plug in allows the creation
15. hen it is necessary to do it This documentation must be updated when the meta model SSME is modified and when a functionality of the Signal ToolBox is added to the SSME Platform 3 Context The Polychrony toolset based on Signal is a development environment for critical systems from abstract specification until deployment on distributed systems It relies on the application of formal methods allowed by the representation of a system at the different steps of its development in the Signal polychronous semantic model It provides a formal framework e to validate a design at different levels e torefine descriptions in a top down approach e to abstract properties needed for black box composition e to assemble predefined components bottom up with COTS Signal is based on synchronized data flow flows synchronization a process is a set of equations on elementary flows describing both data and control the variables of the 04 26 2012 Polych rony Polychrony_SSME_UserGuide Page 5 19 system are signals A signal is a sequence of values which has a clock associated with this clock specifies the instants at which the values are available The Signal formal model provides the capability to describe systems with several clocks polychronous systems as relational specifications Relations are useful as partial specifications and as specifications of non deterministic devices for instance a non deterministic bus or external pro
16. ied Name In Place Editor 5 Paste Ctri V Default Editor Delete Delete x Other Build Path d Refactor Alt Shift T gt 4 5 Connection to Polychrony services To access the Polychrony services under Eclipse the compiler has been deeply connected to the reflexive editor and the graphical environment We obtain a traceability between the SSME models and the results returned by the compiler It becomes possible to show the compilation errors directly on the source model 4 5 1 How does the connection work The connection between the ssME Eclipse editors and the POLYCHRONY compiler is a Java C JNI interface to communicate with the compiler through native libraries The principle of the communication is the following 1 First the SSME model is transformed into the abstract syntax tree AST representation inside the compiler A SSME model parser that makes this translation has been developed 2 Then this AST representation is transformed into an internal graph structure This step consists in resolving all references specified inside the AST checking the type errors and making explicit all implicit clock constraints and clock relations This means that new signals which do not exist in the source model are created The traceability consists in linking each new signal to the corresponding original AST object 3 The third step consists in applying to this graph the different POLYCHRONY services specified in the compilation scenar
17. internal representation of the specification into a textual Java files java files These files are used to simulate the Signal specification It is applied to a graph which must be a sbDC one The graph is with or without clusters Profiling it produces the morphism of the internal representation according to the definitions assigned of the Signal operators given in the ht table into a textual Signal file sig file Lustre it translates the internal representation of the specification into a textual Lustre file lus file Syndex it translates the internal representation of the specification into a textual SynDEx file sdx file for code distribution 04 26 2012 Polych rony Polychrony_SSME_UserGuide Page 11 19 4 3 3 Creation of a compilation scenario The reflexive editor has been automatically generated from the compilation scenario meta model To create a new compilation scenario file ssc right click on your project and select New gt Other and then select the following model Polychrony gt SSME Compilation Model However there are some constraints to create a compilation scenario because some functionalities generators can only be applied after others so an interactive view described in next part has been created to help user to create such scenario 4 3 4 SSME Scenario View The SSME Scenario View see following picture constitutes a way to describe a compilation scenario with some assistance Each funct
18. io clock resolution code generation These operations also modify the graph obtained at the previous step 4 Finally by analyzing the graph obtained after these transformations some errors can be reported in the model 04 26 2012 Polych rony Polychrony_SSME_UserGuide Page 13 19 v 4 Signals Declara_ion Proedc nzd Type integer v Signal Naming Inen itie C 4 Signal Namirg Icen itiec D Description v 4 ReslricL on Process Composition v 4 Signals Defin Lor sclection Parent List rec lable Irze with Columns 2roolems m e Javadoc EA Declsrazion EJ console zrror Log E Propert es SSME Scenario 5 errors 135 war ings 0 others filter matched 106 o 141 items Description Resource a Path Location Type 7 Frrors items ERAOR Double declaration of A AddSub ssme Unkrown ERROR Ident fier nct declared B AddSub ssme SSME Unkrown EMF Problem ERAOR Ident fier nct declared E AddSub ssme SSM Unknown zM l roblem ERROR Missing argumen AddSub ssme SSME Unknowr Problem ERAOR Missing argument AddSub ssme JSSMC Unknown EMT Froblen ERROR Signal B not zeclared in the process interface i Addsub ssme SSME unknown EMF Problem A Hashmap between the Polychrony native AST and the SSME instances has been built in order to associate the node of the native AST where the error message is written and the corresponding instan
19. ionality and generator is represented by a button and according to the functionality or generator you activate others become available or are disabled Problems Javadoc Declaration EJ Console 9 Error Log Properties SSME Scenario 3 Functionalities Generators Scenario none Retiming Boolean to Events Signal Textual SIG Signal Textual LIS Signal Unifications Clock Calculus Signal Textual TRA Signal Model SSME Events to Boolean Abstraction Signal Abstraction Sigali C ANS C Flattening STS M uispiav aii warnings To access to this view select Window gt Show View gt Other and then select Polychrony gt SSME Scenario 4 4 The Signal text editor The SSME environment integrates a simple text editor to manipulate Signal Text files under Eclipse The current version provides only syntax highlighting for Signal keywords for comments and for constant value using primitive types string character or numerical value To use this editor you have only to double click on the file with extension SIG Maybe the Signal Text editor is not selected by default so you have to right click on the file and select Open With gt Signal Text Editor 04 26 2012 Polych rony Polychrony_SSME_UserGuide Page 12 19 Watchdog LIS SIC New gt Open F3 Open With gt Signal textual editor Show In Alt Shift w gt B Text Editor B Copy Ctrl C System Editor ES Copy Qualif
20. ncnsteanemernesiulecseimendeuaceueceteaneavusegouanenedaveenentey 3 2 SUIS M 9 E 4 2 1 Purpose of the ore duo p MR 4 2 2 Editing particularities 4 2 2 1 Changes IAS nilieciis gU 4 2 2 2 Temporary CAMINO seccccscscsncczsseremesnsreenescoveresnmavdceesomlernienenetdenedasetoeneteneumuavevevantads 4 ZS Application SCONE eL T 4 2 4 Edition and evolution of the document eee 4 S CONTEXT acne es Zeca oma chase MES DI Map AM M NM LM MIN SM MISCO Matas tone A 4 4 Using the SSME aedem M cH 6 4 1 Creation of a new PNG SCI ciui ook qup MER Rcx PepANU DUAM DER Uu RR RD REDE rau tUe cO ROS Cdi Mid DURS 7 4 2 Creation of a new SSME Modlel 5 arcte rnt Rara RRkR a osa A aaa hase dbuniadstedsddas 7 4 3 The compilation SceriariOS atsacs ciassadacdsnideitvanistiindaaedaa Maaadatuaniee dang ddaasuaaaaacdaanieaes 8 4 3 1 Sgen 8 43 2 GENeratOrS te EA 9 4 3 3 Creation of a compilation scenari o eeeeeeeeeeeeeee nnne 11 4 3 4 SSME SCCMMANO VICW E 11 4 4 The Signal text SCOR ect 11 4 5 Connection to Polychrony SCMICGS iiscaiccisiccusacisaasadenslaiseianaasdbiandaolanneddeneiuepenanaks 12 4 5 1 How does the connection work eeeeeeeee eese enne 12 4 5 2 Compiler CONMQUMAN ON EL
21. nt is available in a plug in directory named e fr irisa espresso ssme polychrony win32 win32 x86 for Windows x86 e fririsa espresso ssme polychrony win32 win32 x86 64 for Windows x86 64 e fririsa espresso ssme polychrony gtk linux x86 for Linux x86 e fririsa espresso ssme polychrony gtk linux x86 64 for Linux x86 64 e fririsa espresso ssme polychrony cocoa macosx x86 for MacOS X Intel x86 e fririsa espresso ssme polychrony cocoa macosx x86 64 for MacOS Xj Intel x86 64 By default this parameter only contains the root of this lib directory For example if you want to use the apex arinc library add to the parameter the path lt lib directory gt apex_arinc653 lib e Maximum number of types This parameter represents the maximum number of types that can be loaded during a compilation Default value is 4096 e Memory size for the internal structure This parameter represents the memory size reserved for the allocation of the internal tree structure used during a compilation Default value is 60000000 bytes e Memory size for the string structure This parameter represents the memory size reserved for the allocation of strings Default value is 1 Mb If you change one of these values validate these changes by clicking on the apply button For restoring the initial values click on the Restore Defaults button 04 26 2012 Polych ro ny Polychrony SSME UserGuide Page 15 19 4 5 3 Applying Polychrony services To call Polychrony servi
22. tor interactive access to compiling functionalities Signal GUI requires the Signal ToolBox or an other component that redefines the Signal ToolBox Apls The SSME PLATFORM a front end to the Signal ToolBox in the ECLIPSE environment SSME PLATFORM requires the Signal ToolBox or an other component that redefines the Signal ToolBox Apls SSME stands for Signal Syntax Model under Eclipse The POLYCHRONY TOOLSET also provides 04 26 2012 Polychrony Polychrony_SSME_UserGuide Page 6 19 libraries of SIGNAL programs a set of SIGNAL programs examples user oriented and implementation documentations facilities to generate new versions AADL Synoptic Signal Graphical Format NS Signal SyNDEx C Sigali Cr Lustre Java Dot Illustration 1 Polychrony tool set 4 Using the SSME Platform PE SSME user guide is composed of the following sections Creation of a new project Creation of a new SSME Model The compilation scenarios The Signal text editor Connection to Polychrony services 04 26 2012 Polychrony Polychrony_SSME_UserGuide Page 7 19 4 1 Creation of a new project If you have no project in your workspace you will need to create a new one Right click on the navigator view select New gt Project Select then a General project this will be sufficient to model and click on Next gt Give a name to the project and click on Finish 4 2 Creation of anew SSME Model To help the user during t
Download Pdf Manuals
Related Search