Home

Guided Tour

1. 16 Figure 12 EDICT Instantiating the Complete Avionics System Implementation 17 Figure 13 EDICT Displaying the EDICT Design Perspective sss 18 Figure 14 EDICT Importing AADL Model into EDICT seen 19 Figure 15 EDICT Initial to Final Avionics Architecture Pattern sese 20 Figure 16 EDICT Reset Pattern Application to Initial System eeessssseeeseese 21 Feur 17 BDICT Repheate POS ACG ibis tesisupbn PES NvIF ope tes tes uix Ed IUD nanoiniess 22 Figure 18 EDICT Insert FGS Leader Selection Pattern eeeeeeeeeereeereererrerrrerrrererrerrrrrrrrrrerees 23 Figure 19 EDICT Apply PALS to FGS Leader Selection Pattern ssesseeesees 24 Figure 20 EDICT Insert Guidance Command Selector Pattern sss 25 Figure 21 EDICT Replicate Pitch Sensor Pattern eeeeeseseeeeeeeeeeeeeeennnnnnns 26 Figure 22 EDICT Insert Pitch Voter Pattertisuiuesi ioo berto os pets ee pues read is usate petes 27 Figure 23 EDICT Replicate Airspeed Sensor Pattern eese 28 Pigure 24 EDICT Insert Airspeed Volet Pallet etai rre Io iara Ret o9 usar nexu puta 29 igure 25 BDIC T Replicate ADS Tate EB ades uq ed etu e UE ERU eens aca HU utes id UR U AE boOd elus 30 Figure 260 DBDICT ROpliedte AHS PO OE flos secs prMN E RISUS E 3l Figure 27 bDICT Repl
2. SA Conbrol Surface Acbusbor Data FD Guidance Dara FD enl Guidance ata oh FM Fight Management Data FM ipl Flghz Management Data HAY Miriga Data FOS LS sa FOS Fe LH G FOS RAEO m FOS LE A y MAN cpy 2 Miga OA mmm Up afit WORE Yoke Data Shhh hhh eae T i b B Mat s EE l i 1299 d Prog Cal eripe Pan x b isl 4 x aage d Fip Controt System tp M 4 s spem BEBE L j al Ready Flight_Contrel_ Sytem imp j G car NUM SCRL WAN Figure 44 SysML Redundant Flight Control System O Copyright 2011 Rockwell Collins Inc 48 All rights reserved GUI DED TOUR DEMONSTRATION OF THE TOOLS ims Collins Next navigate to and open the ibd for the Avionics System as shown in Figure 45 As you can the new subsystems created during pattern application are now present However some manual editing 1s still needed For example the connections from the new subsystems on the right need to be manually connected to the new ports on the Flight Control System FCS 3x Bao 2 43 t 1 a a H Bel property ADS Ar Dit System H GS property ADSR r Dia System me property AR Atitude Heading Symm WB Gey property AR Altitude Heading Syd Es lt property CSA Control Salaca Achastore KS 98 v MO P rb ji OPAN b S iN D Esp property FCS Fight Control System a im D D D 4
3. Apply button in the Pattern Transform window This pattern will replicate the Flight Guidance System FGS in the Flight Control System FCS along with its connections and the ports on those connections as shown in Figure 17 EDICT Design META Design Cffort SysComp teem core archtecture pattermns transforms Initial to final Avionics System sysptml D1CT Core Tool Suite F e Edt Newipste Search Project EDICT Run META Window ie es Jer fee eto oe CY BR evict Design AAA Qo Resource Regi ate FGS Insert FGS Leader Selection Apply PALS to PGS Leader Selection Insert Galore Command Selector Replicate Pitch Sensors Insert Pach Voter Replic abe Arspeed Sensors Insert Airspeed Voter Brod ste ADS Replicate AHS Replicate PMS Regie ote NAY Replicate PFD Rep ste Yoke Replicate Throtties Replicate Processor ii ew Architecture Frameworks Sz META Archtecture Frame ie Data Libraries T Logical Architectures E System Architecture Trai i System Architectures 2 Intia Avionics System 3 initial Aviorics System ME 3 System Architecture Auge 34 Architecture Traces cU patterns e Arch Pattern Transf cazon orane vy 2 SSeS Se 0112 1212 012 1 lt eyna uyu intial_to T Sys Arch Pattern Trans Behavior System Architecture v amet d Augmentation Imported Model Status v Current ER eme nen Figure 17 EDICT Replicate FGS Pattern O Copyright 2011 Rockwell Collins Inc 22 All
4. Pan Oviput 3x M 4 b W System ASeret 7 Ls j gt j ag Personal information O Project Information ibd SytML Internal Block flight Guidance System Imol Flight Guidance System ImetFlight Guidance System impi ph Guidance Proce op G CAP NUM Figure 6 SysML Flight Guidance Process FGP The Flight Guidance Process consists of a Mode Logic ML and Control Laws CL component These components are stereotyped in the model as an AADL threads Since this is a system architectural diagram no further information is provided about these components The implementations of these leaf level components will be specified outside the system architecture model In complete system architecture a contract would be specified for each thread defining the assumptions the thread makes about its environment and the guarantees the thread provides to its environment The guarantees correspond to the requirements that must be satisfied by the component implementation Next we will review the internal structure of the hardware component of the Complete Avionics System the IMA Platform Visible in the SysML block diagram located directly under the FGS package O Copyright 2011 Rockwell Collins Inc 11 All rights reserved GUI DED TOUR DEMONSTRATION OF THE TOOLS Rockiwe 21D xj iP b gt LJ b D 8 S att amp E Ad dj Esie Normal 5 File Edit View Project Diagram Element Tools AnMyser Addins Settings Wind
5. 2 3 t 9 El Profile 9 Enterprise Architect ws Workspace Layout Racie Normal R intis avionics System P3 Protile 4b Stereotype Qj Metactess 2 j Manage Project 5 Recent Jj Enumeration E a9 Open a Project File initial Avionics System Create a New Project Firnal_Avionics System 9 ir A iz __ Copy a Base Project Connect to Server o 50 6 i 3 3 8 amp Common Help Open Learning Center Use tne Learning Center 4 Introdurtion to Models Creme a Project D Server Repository Online Betources amp Tutorials Enterprise Architect Commun Ry 4 Q3 Start Page tput M a M System Soret 7 Lal j E ba Pertonal information Project Information Ready Figure 1 SysML Initial Avionics System Model Copyright 2011 Rockwell Collins Inc 6 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins Expand the package for TOP in the Project Browser window on the right side until you see the icon for the SysML Internal Block Diagram ibd labeled Complete Avionics System located under the icon for SysML block labeled Complete Avionics System Impl Double click on the icon for the Complete Avionics System ibd This should open the image shown in Figure 2 Project Browser Bau m a d t9 B m Inicial Avionics System Pet zd Connector Part Distributed Pact c Plow Part c Pathipaet Part G Signal 29 Pot 9 Ponpes gt Fl
6. 31 2 ael Comment B ond gt Comment Permiion amp hrensiry granted Free of charge te ary person obtaining iE packaget Comment acopy pf this daas including any solbeare or models in source or ir ADS D 4k Comment bibr Form 26 well at any deeds spechecabont and uta de Commend beure r oikea a Dus a babaa i hee Gustin wkl Bi APS not a Comment restriction mudeg without imitation ter rights house copy F A5 end Comment mod y merge publich de tribube subicere andfor csl copies of ig Css aac Comment the Dish Mwin peremit persone boc whem Ehe Daba is Furnished En ee li PCI Comeent s abiat bo Hee fokig c ndibions g POS pat de Conn ward li FOS next gt oComment The above copyright notice and thir permission notice shall be lg EME aad Consent included in al cops cor subetantisl portionis of Ehe Data ri IMA aat de Comme FI MAN Sal Comment THE DATA 15 FROVIDED 5 15 WETHOUT WARRANT OF AME RIND EXPRESS DR li PPD eect Comment DAPLILG IHCLUDING ELIT NOT LIMITER TO THE WARRANTIES COP F THECTTUE akdi Comment MERCHANTARILETY FITNESS FOR A PARTICULAR PURPOSE AND NONINFRENGEMENT lg TOR Complete Anioris Syste Comment EMO EVENT GHALL THE AUTHORS SPONSORS DEVELOPERS CONTRIBUTORS C ri TOR aao 4 Com wn COPYRIGHT HOLDERS EE LEARLE FOR AHV CLAIM DAMAGES CR OTHER LTABRLTTY ld THES ardi Comment WHETHER IN AN ACTION OF CONTRUARCT TORT OR OTHERWISE ARTSING FROM Ca YT aad Comment OF OR IN CONNECTION WITH T
7. Ge Figure 7 IMA Platform HW The Integrated Modular Avionics IMA Platform describes the hardware architecture onto which the Avionics System software will be mapped It consists of a Fast Common Computing Module CCM A a Slow CCM B and an IMA Bus Note the direct access connections to the IMA bus 1 e the absence of ports on the bus For this to be translated correctly into AADL the End System ES ports on the CCMs must be stereotyped as AADL requires bus access ports This concludes the exploration of the Initial Avionics System SysML model Feel free to explore the rest of the model on your own Additional information about the Initial Avionics System and SysML can be found in the Final Report and in the SysML AADL Translator User Manual In the next portion of the tour we will import the Initial Avionics System SysML model into AADL and the EDICT tool O Copyright 2011 Rockwell Collins Inc 12 All rights reserved GUI DED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins 3 Importing the Model In this portion of the tour we will import the Initial Avionics System SysML model into both AADL and the EDICT tool If you do not have EDICT installed or do not have a current license you can import the model as described in this section using the OSATE tool instead Then proceed to Section 6 for demonstration of the verification tools To simplify the import process we have provided a workspace for the EDICT tool tha
8. META Design Effort Design Option META Design Option d Initial _Avionics System E ET System Architecture Auc pe B Architecture Traces P Patterns B a Sys Arch Pattern Trar Initial to Final 2 System Composer b New b Pattern Instantiations Replication Leader Select PALS Voter Insertion Replication Voter Insertion Replication Voter Insertion Replication X EDICT Design META Design Effort SysComp team core architecture patterns transforms Initial_to_ Final Avionics System syspEml EDICI Core Tool Suite REE Replicate FGS Insert FGS Leac Apply PALS to F Insert Guidance Replicate Pitch Insert Pitch Vot Replicate Airspe Insert Airspeed Replicate ADS System Architecture Initial Avionics System All PIs Applied B Outline Arch RISISI SI SISSY S Replication Replicate 4HS Imm lm m fnm m ami on on fnm FRIC m Add Edit Remove Transform Control Apply Reverse Reset Apply All Y Logical System System Architecture v Import amp Augmenta gt Imported Model Status v Current View Details Import Control Import canet View Lo Import Preference Manua Import Status import not sunning Model verification results are not available Figure 35 EDICT Open Architecture Browser Select the transformed model that you just saved SE Open Model Select a
9. nen 4 Comment of the Defense Advanced Research Projects Agency DARPA i Comment aa 4 Comment Permission is hereby granted free of charge to any person obtaining p 4 Comment a copy of this data including any software or models in source or j v Comment binary form as well as any drawings specifications and i e Comment documentation collectively the Data to deal in the Data without j Comment restriction including without limitation the rights to use copy me Comment modify merge publish distribute sublicense and or sell copies of j un Comment the Data and to permit persons to whom the Data is furnished to do ke Comment so subject to the following conditions j a Comment ges 4 Comment The above copyright notice and this permission notice shall be j m Comment included in all copies or substantial portions of the Data A Comment j m Comment THE DATA IS PROVIDED AS IS WITHOUT WARRANTY OF ANY KIND EXPRESS OR x 4 Comment IMPLIED INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF j mm Comment MERCHANTABILITY FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT S 4 Comment IM NO EVENT SHALL THE AUTHORS SPONSORS DEVELOPERS CONTRIBUTORS OR j DE Comment COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM DAMAGES OR OTHER LIABILITY pes 4 Comment WHETHER IN AN ACTION OF CONTRACT TORT OR OTHERWISE ARISING FROM OUT j dead Comment OF OR IN CONNECTION WITH THE DATA OR THE USE OR OTHER DEALINGS IN THE Figur
10. Composition L Replace FGS Core 2 Insert FGS Leader Selection el E Architecture Frameworks 3 5 Apy PALS to PGS Leader Selection g META Architecture Frames f x Insert Gabon Commarid Selector 0 Data Libraries Replicate Pitch Sensors TP Logical Architectures Insert Pech Yoter a BE System Architecture Trand Replicate Rie speed Sensors System Architectures Insert Airspeed Voter TF Intia Avionics System Pool ste ADS 3 initial Avionics System ME Replicate AHS ES System Architecture Augie Replicate PMS 34 Architecture Traces 2 D Rogie ote NAV Patterns 3 Replicate PFD E Sys Arch Pattern Transft v Replicate vokas in Device T anitial to Final Avionics Pepkate Theottles T Sys Arch Pattern Trash Replicate Processor Behavior System Architecture v ameet cb Augmentation Imported Model Status v Current View Detats Import Control Import Preference Manus Import Status NONE ant NDADI Figure 15 EDICT Initial to Final Avionics Architecture Pattern EDICT will open the Pattern Transform window and apply all the pattern instances to the imported model O Copyright 2011 Rockwell Collins Inc 20 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS dem os f Collins To study the pattern application more carefully click once on the graphical display of the mode then use the mouse scroll wheel to size the image to fit in the window Then click the Reset button in the Pattern Trans
11. EDICT Insert FGS Leader Selection Pattern O Copyright 2011 Rockwell Collins Inc 23 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Apply the next pattern by pressing the Apply button This pattern applies the PALS pattern to both Leader Selection threads While this does not change the graphical display of the model it does add AADL properties to the model that implement the PALS logical synchronization protocol The pattern also adds contracts to the model that will satisfy the assumptions of synchronous operation that are made by the Leader Selection pattern EDICT Design META Design Cffort SysComp teem core archtecture pattermns transforms Initial to final Avionics System sysptml D1CT Core Tool Suite F e Edt Navigate Search Project EDICT Run META Window Heb e PQ es Ei rto CY BR eor design Shaa IS Resource EJ EOT Design Workspace D 5 3 Intel to Pinel Avionic EV Design Effort META Design Effort Design Option META Design Option 7 oc System Composition S core EV Architecture Frameworks META Architecture Franev ie Data Libraness T Logical Architectures a SE System Architecture Trans System Architectures TT Intia Avionics System Rekaan Repicate FGS Leader Select Insert FGS Leader Selection PALS Apply PALS to PGS Leader Selection Voter Insertion Insert Gambie Commarid Selector Reckcoton Replicate Pitch Sensors Voter Insertion Insert Pach Voter Regie ation Rep
12. Leader Selection Insert Gaadorce Command Selector Replicate Pitch Sensors Insert Pach Voter Replicate Arspeed Sensors Insert Airspeed Voter Replicate ADS Replicate AHS Replicate PMS P epic ote NAV Replicate PFD Repke ste Yokes Replicate Theotties Replicate Processor ii ar Architecture Frameworks Sz META Archkecture Frame ie Data Lbs T Logical Architectures 8 BE System Architecture Tract i System Architectures 2 Intia Avionics System v G uo e wv 3 initial Aviorics System ME 3 System Architecture Auge 34 Architecture Traces c O8 patterns e ss Arch Pattem Transft initis to Final Avionics 72225272 PhRRPEPPRRPRES CXIC cua T Sys Arch Pattern Tras Behavior System Architecture v ameet cb Augmentation Imported Model Status v Current View Detats Import Control Import Preference Manus Import Status import vt runang Figure 23 EDICT Replicate Airspeed Sensor Pattern O Copyright 2011 Rockwell Collins Inc 28 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Apply the next pattern by pressing the Apply button This pattern inserts a voter that selects the medial value of the three airspeed sensors ei Q 9 ri et Oe CY BR evict design gp AMO Resource Design Effort META Design Effort Design Option META Design Option Replace FGS Insert FGS Leader Selection Apply PALS bo PGS Leader Selection Insert Gabon Comenansd
13. Model to View Please select a model File to view in the Architecture Browser Patterncopw Initial Avionics System Initial Awvionics System META Design EFFart META Design Option _Full4T Initial Awvionics System Figure 36 EDICT Select Model for Architecture Browser O Copyright 2011 Rockwell Collins Inc 40 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Om Ins The Architecture Browser provides several new views of the system On the left side of the main panel you will see a pull down menu for Select View Choose the Properties Viewer option This view will display AADL properties for each model component Select one of the Leader Select LS components either by clicking it in the diagram or by using the model tree on the left side of the main panel as shown in Figure 37 Now we can see the new properties that were added by the PALS pattern X EDICT Design META Design Effort 5ysComp team core architecture system PatternCopy Initial Avionics System archsysml EDICT Core Tool Suite File Edit Navigate Search Project EDICT Run META Window Help J S 4 95 t0 m ES nd T AADL 0 Resource System Architecture Model Properties Viewer El System SW b Device CSA Device YOKE Device THROT El System FCS E System AP E System FCI B System FGS j l Process FGP Thread ML i Thread CL Thread LS i E System FGS_R E System PFD E System AHS Er
14. Selector Replicate Pitch Sensors Insert Pach Voter Replicate Arspeed Sensors Insert Airspeed Voter Beo ste ADS Replicate AHS Replicate PMS Regi ote NAV Replicate PFD Repke ate Yoke Replicate Theotties Replicate Processor E BY Architecture Frameworks Sz META Archkecture Frame ie Data Libraries YP Logical Architectures 5 E System Architecture Trandz i System Architectures 2 Intia Avionics System o G uu 9 wv 3 initial Aviorics System ME 3 System Architecture Auge 34 Architecture Traces c O8 patterns eM ss Arch Pattern Transft 72225272 Sere Perro 444 ns 4 cua T Sys Arch Pattern Tras Behavior Imported Model Status v Current View Dotas Import Control Import Preference varo Import Status import vt runang Figure 24 EDICT Insert Airspeed Voter Pattern O Copyright 2011 Rockwell Collins Inc 29 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Apply the next pattern by pressing the Apply button This pattern replicates the entire Air Data System ADS including the replicated pitch and airspeed sensors with their voters to create a redundant ADS function n META Design Cffort SysComp team core archtecture pattermns transforms Initial to Final Avionics _System sysptmi DICT Core Tool Suite Pie Edt Navigate Search Project EDICT Run META Window Heb Jer SQ 9 et Oe Cy ER evict on SPAA Resource l Te Design Effort MET
15. System FMS j l Process FMP i Thread FMT F System ADS i System i System i System FJ System l system PALS Group Name FGS Leader Selection Paysan PALS Period 50 0 ms Device YOKE R Device THROT R E System Hw Figure 37 EDICT Properties Viewer in Architecture Browser O Copyright 2011 Rockwell Collins Inc 41 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS dem ms ns 5 Exporting the Model At this point we are ready to export our transformed model out of EDICT back into AADL OSATE and then back to SysML for final editing Select File Export from the main menu This will display the screen shown in Figure 38 In the Export window that pops up expand the Other folder select AADL Mi ac Instance and click on the Next button Em 2 1npi x LE a y ES B Ente neg SS ARDS Besse EJ EDICT Design Workspace 7 DTI EIU Design Effort META Design Effort Design Option META Desin Coni Capture the Current Stabe of the System Archibecture fs System Compasitinn F Core Brchitecture Franek MET 2echitechune France Data Libraries F Logical Anchitectures E Stem Archibechung Track t5 System Architectures tom liia focuses Systees tc Imi funis system ME sos Patento nid one 2 Systorm Archilos tuni Aue 1 architecture Traces pattern Sr Arch Paltar Trareh 1h Inii ko Final Avioni Se Arch Pattern Transit Behavi
16. UML SysML tool for constructing and editing system architecture models This is a commercial tool but you can download a trial version to use for the demo 2 EDICT System design and analysis tool that hosts our architectural design pattern functionality This is a commercial tool developed by WW Technology Group but an evaluation license has been included with the distribution 3 OSATE An open source tool for constructing and editing system architecture models in AADL This tool may be used as an alternative to the EDICT tool as a way to access the functionality of our other META tools but the design pattern functionality will not be available 4 Rockwell Collins META plug ins Translation and analysis tools for system architecture models These tools are provided as plug ins for both the EDICT and OSATE tools a SysML AADL model translator b Lute tool for checking structural properties of AADL models c AGREE tool for compositional verification of AADL models 5 Kind model checker Model checking engine used by the AGREE tool Kind is an open source tool developed by the University of Iowa We have also provided a collection of example models of an avionics system in both SysML and AADL formats These models and their use will be described in the course of this Guided Tour The Guided Tour will lead you through the following steps Examine an initial version of the avionics system model in SysML Translate the model i
17. for AADL System Instance O Copyright 2011 Rockwell Collins Inc 44 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins This has exported the AADL system instance of the transformed model and has also modified the AADL declarative model of the Initial Avionics System model to be consistent with the transformed model Normally the OSATE tool would also update the textual AADL to be consistent with the updated AADL declarative model However this capability is not implemented in the alpha version of OSATE 2 currently available For this reason a few more steps are needed to export the transformed model to AADL and OSATE First select the AADL Perspective button in the upper left hand corner to switch to the AADL perspective Then before cleaning the AADL model select the Initial Avionics System model in the AADL Navigator window shown on the left in Figure 41 and select META Generate AADL from the main menu bar This will generate the textual AADL to be consistent with the AADL declarative model Finally select Project Clean for the Initial Avionics System model to recompile it and check for errors Since the Initial Avionics System model is really the transformed model you may wish to use the File Rename function to rename it to Final Avionics System S AADL META Design Effort SysComp team core architecture petterns transforms Initial to final Avionics System sysptml ED
18. gj vo 4 PR Notes B Prep Toc W Prey Seri A Pan ibd SytML Internal Block Flight Guidance System Imol Flight Guidance System ImptFlight Guidance System impi Flight Gusdance System L lot cae NUM SCRL wan Figure 5 SysML Flight Guidance System FGS The Flight Guidance System consists of a single Flight Guidance Process FCP component This component is stereotyped in the model as an AADL process It provides a single address space shared by all the software components for the Flight Guidance System Next we will review the internal structure of the Flight Guidance System Process FCP While this stereotype is not visible on the ibd it can be seen be seen on the SysML block diagram located directly under the FGS package See the SysML AADL Translator User Manual for more details O Copyright 2011 Rockwell Collins Inc 10 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins Navigate to and open the Flight Guidance Process ibd as shown in Figure 6 2 5 xj Esu LJ ih D e X att amp E Ad fj Esie Normal E File Edit View Project Diagram Element Tools AnMyser Addins Setting Window Help DITENNUXE uL S CAFEER B SysML Block Internal gy Ins Avionics System 2 Part g aos Gb Conmector Part bi pe ed Distributed Part m a cd Plow Part s gj cs cj Participacit Part gj rea Signal gj rcs d s j Pos 2 Pot 9
19. grga Available System Architectures t Indie Avionics Sysbem ts rtia fated Cyber ME T3 PatkemCopy Irtis Avion Er System Archinect Bun ae Architecture Traces patterns EH Sys Arch Pathan Trach _ Rr initial to Final Avionics i Saye Anch Pattem Transat Behavior Sys bem Architecture v ampet o tgrenttion Irrgser benc Model Stabu A Curnent Import Contre tret Preference Marua Import status mpoet oc nonni Model verification renuks ane not analisblie L D Mija Vatikaan 21 SF Enor wal Figure 39 EDICT Select System Architecture to Export O Copyright 2011 Rockwell Collins Inc 43 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins Another pop up window will appear asking you if you want to write the AADL instance mode to an existing instance or create a new instance Select Create a New System Instance Another pop up window will appear adding you to where to create the new system instance You must create the instance in the aaxl package structure of the Initial_Avionics_System Expand the Initial Avionics System folder in the pop up window then expand the aaxl not the aadl folder and select the packages folder as shown in Figure 40 Finally type in Final Avionics System as the name of the AADL system instance click on the Next button and then click on the Finish button META De ii x E r a e m R
20. ig Tapped raea ll Sergiy CL ena El Profile 39 Entergrise Architect ves s Workspace Layout Base Por P3 Praile dP streetype CI mnetadasi Manage Projects Recent L3 Open a Project File D Final avionics Syrie Create a Hew Project J Initial Auienic Sycbem Cepy a face Prajert 4 enne to Server Help Open Leaning Center S Use the beaming Center d introduction t Models D Chim amp Project 4 Server Repository Online Bergarar B Tubesialt Enberpriet Bachited Community WF WN sytem erat L a fg Persanatinrermaten Qi Frojea womans Peacy ien Oe ae A WaN Figure 43 SysML Open Exported SysML Model Copyright 2011 Rockwell Collins Inc 47 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Navigate in the Project Browser window on the left to the Flight Control System Impl and double click on the ibd icon to open the diagram as shown Figure 44 As you can see the new replicated FGS along with its ports and connections is now part of the transformed model once System Alber Patbenn Application A P dp Erie Normal e Avioni i AW ae Bye RUE E WELL r i File ect ee ee a a T Aioni Sytem After Paktem Appias amp Exported System E g aps i 4 1 J 3 I F spsFDL Fot OC Je FCE amp FO apyl n Bm AD Ar Data AD cpyl Ar Data Abl Aiie Meade Data a AH pyl Altitude Heading Dara
21. other side to be the leader During these steps the pitch values on the right side drift downward while staying within the 1 0 bound of previous values In step 4 the right FGS becomes active and reports 0 3333 as its pitch value In step 5 this value 1s picked up by the autopilot which previously was using the stale value of 4 8 This results in a pitch delta which exceeds the 5 0 bound similar counterexamples can be generated by removing other facts about the leader selection such as the property that a leader always exists or the property that when the leader fails leadership is transferred to a non failed node 8 2 Allowing Immediate Re failure The flight control system has an assumption that when a FGS recovers from failure it does not fail immediately in the next step assume prev prev not FD L mds valid false false and prev FD L mds valid false gt FD L mds valid assume prev prev not FD R mds valid false false and prev FD R mds valid false gt FD R mds valid O Copyright 2011 Rockwell Collins Inc 56 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Hockwe Co ns If we remove this assumption the following counterexample to the system level guarantees 1s generated Signal Type AD_L pitch val AD_R pitch val AP CSA csa pitch delta AP GC L cmds pitch delta AP GC L mds active AP GC R cmds pitch delta AP GC R mds active FGS L GC cmds pitch delta FGS L GC mds active bool FGS
22. rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins Apply the next pattern by pressing the Apply button This pattern inserts a Leader Selection thread and many of its connections inside of both copies of the FGS to ensure that only one FGS is ever active at the same time It also inserts a contract formally specifying the behavior of the Leader Selection thread EDICT Design META Design EfTort SysComp team core architectur m F e Edt Navigate Search Project EDICT Run META Window Help Hr Iv iE eal to coe CY BR evict Design AAA Qo Resource Repi ate FGS Insert FGS Leader Selection Apply PALS to PGS Leader Selection Insert Gamborwe Command Selector Replicate Pitch Sensors Insert Pach Voter Replic abe Arspeed Sensors Insert Airspeed Voter Bod sm ADS Replicate AHS Replicate PMS Regi ate NAY Replicate PFD Rep ste Yoke Replicate Throtties Replicate Processor ii ew Architecture Frameworks Sz META Archkecture Frame ie Data Libraries YP Logical Architectures L E System Architecture Transi i System Architectures 2 Intia Avionics System 3 initial Avionics System ME 3 System Architecture Aux 34 Architecture Traces cU patterns e Arch Pattern Transf cazon orane vy N LIIS 1211 12 12 2 012 E SES eyna uyu intial_to Wi Sys Arch Pattern Trask Behavior System Architecture v ameet Augmentation Imported Model Status v Current Figure 18
23. 0 6 0 33333 0 166667 AP CSA csa_pitch_delta real O 0 066667 0 133333 0 1 4 733333 0 26667 AP GC L cmds pitch delta real 0 4 8 4 933333 0 46667 0 13333 0 06667 AP GC_L mds active bool TRUE TRUE FALSE FALSE FALSE FALSE AP GC R cmds pitch delta real 0 3 933333 4 866667 0 4 0 533333 0 33333 AP GC R mds active bool TRUE FALSE FALSE FALSE FALSE TRUE FGS L GC cmds pitch delta real 4 8 4 933333 0 46667 0 13333 0 06667 0 066667 FGS L GC mds active bool TRUE FALSE FALSE FALSE FALSE FALSE FGS L GC mds valid bool TRUE TRUE TRUE FALSE FALSE TRUE FGS L LSO leader int 3 2 2 3 3 2 FGS_L LSO valid bool TRUE TRUE TRUE FALSE FALSE TRUE FGS R GC cmds pitch delta real 3 933333 4 866667 0 4 0 533333 0 33333 0 03333 FGS R GC mds active bool FALSE FALSE FALSE FALSE TRUE FALSE FGS HR GC mds valid bool TRUE TRUE FALSE TRUE TRUE FALSE FGS HR LSO leader int 3 1 0 1 2 0 FGS R LSO valid bool TRUE TRUE FALSE TRUE TRUE FALSE leader pitch delta real 0 4 8 4 8 4 8 4 8 0 33333 Note that the value of the leader variable makes sense only when the corresponding side is valid otherwise the value is arbitrary A leader value of 1 corresponds to the left side while 2 corresponds to the right side In step 0 the left FGS is active and report a pitch value of 4 8 while the right FGS is inactive with a pitch value of 3 4 within the 2 0 bound of the other side Then in steps 1 2 and 3 neither FGS puts itself in the active state since it 1s either invalid or it believes the
24. 2 as Js Participant Part a block Aviones System T signa P un gt Avionics System Imol 9 Pot P M lt property 2 ADS Ar Deka System E Port iow 5a property AG Aude Headng System 9 Flow Specification St property CSA Control Surface Actastors me property FCS Fight _ Control System B y m me property FMS Flight Morugeement Syster LS A E property NAV Nevapation_ System Ee property PFO Priswy Fit Depley E Profile V E propertys THROT Theokttle E Profile V E spropertys YOKE Yoke D CSA 4b Stereot al ypt a Dra 5 Nhetactess iu FCS Ls Enumeration D rcs s GB ees El Common a gj mA 2AB 2 25 5u08 5 8 neome gj roe 3 8B E tee I3 FS ia yout ze THR TFCE 2 YOKBNFCS xj 4 J 15 6 Sart Page d as e Notes eoo iis W Prey O Sent e Pan Oviput M 4 M System ASeret 7 L j gt j bg Personal information O Project Information Ready E etm CAP NUM AN Figure 3 SysML Initial Avionics System SW As shown in Figure 3 the Avionics System software consists of several subsystems such the Flight Control System FCS the Primary Flight Display PFD and the Control Surface Actuators CSA This Initial Avionics System example is a sunny day design that assumes no component will ever fail so there are no redundant components to provide fault tolerance In Section 4 we will add components to implement fa
25. 2 sas 9 Port how Flight Guidance Process Ilmpl u block Capture Condos 9 Flow Specification gj block Control Laves block Control Lave Imgi El SysMI Block internal ad block Fight Guidance Process 7 3 ta Mj block Flight Guidance Process Tmgl dd Fia Gukteece Process Impi Bl Profile 4 sllosvort AD P Profile 4 sllowPort AH Altiuse Heading Dota E AE flow Port FCT Fight Crew Interface Di p Stereotype J sllowPort GC Gusdorce Dota E Metactass 4d fiowPert NAV Navigation Data ij Enumeration 4d fiowPort VNAV Flight Management Dal V WS propertys CL Control Laws 8 X md property ML Mode Look AAE G 3 Bj bock Fight Guidance System Mj block Fight Guidance System fmol aoso Bj block Fight Modes 3 Mj block Fight Modes ingi a 3 8B il block Guidance Commands LE ME Mj block Guidance Commands Img ll block Guidance Data E block Guidance Data 1moi lg block Lateral Modes lg block Lateral Modes Impl lg block Made Logt ld block Mode Loge imel lg block vertical Modes ld block Vertical Modes Imol a gj res 5 gj ma lu Nay uj pto 9j THROTTLE TOP gj TEs D aj YOE zi re 04 4 b E COMPILE oic System i Flight Control System E Fight Guidance Systems imp t Flight Guidance Process Impl b muss Prop t Tas E GE A Seri
26. 30 September 201 1 Design Documentation Guided Tour Complexity Reducing Design Patterns for Cyber Physical Systems Prepared for DARPA TTO META Contract FA8650 10 C 7081 Technical Point of Contact Business Point of Contact Dr Darren Cofer Mr James Steggall Rockwell Collins Inc Rockwell Collins Inc 7805 Telegraph Rd 100 400 Collins Rd NE MS 121 200 Bloomington MN 55438 Cedar Rapids IA 52498 Telephone 319 263 2571 Telephone 319 295 3107 ddcofer rockwellcollins com jistegga rockwellcollins com DISTRIBUTION STATEMENT A Approved for public release distribution unlimited Rockwell Coffrns Rockwell Collins Inc 400 Collins Rd NE Cedar Rapids lowa 52498 Copyright 2011 Rockwell Collins Inc All rights reserved GUI DED TOUR DEMONSTRATION OF THE TOOLS Rockiwe Collins Table of Contents DiI 5 2 JNSeviewins the vs Vb Node seas sacs RER eta getasese timuit ette e spei stu 6 3 mbpotins The MOUCL scooter nen E E ne ee meee ee re ene 13 4 Applying Patterns to the MOG Gliis csvsssssencnnncsnasdonnedesiwareqaaseontne cnnecaekeansatinntenteasaiunstonreesawantees 20 BO tie dVode Lacscisseeudntt E sone amen astaaneresaeuonnee man SRM E C UNUS d UEUE 42 6 Verification or the Final Avionics System eec oett rior beo eie Patet euentu vau ui uc En E NuUa QUE 50 J Umem Eute tuetur Chee KOE EE op 51 o Usine the AGREE Model Checking TOON isi ccsceccscvavacescedvvesecaessscaearecaes
27. A Design Effort Replace PGS Insert FGS Leader Selection Apply PALS to PGS Leader Selection Insert Galore Command Selector Replicate Pitch Sensors Insert Pach Voter Repicate Arspeed Sensors Insert Airspeed Voter Replicate ADS Pepkcate AMS Regkcate PMS Rogie ote NAV Replicate PFO Regie ste Yokes Replicate Theotties Replicate Processor te Ed Architecture Frameworks Sz META Archkecture Frame ie Data Lirias 1 Logical Architectures 8 BE System Architecture Trandz i9 System Architectures 2 Intia Avionics System 3 initis Avionics System ME 3 System Architecture Aux 13 Architecture Traces c OU patterns e z Arch Pattern Transft snrsaonease eeanew a OO Oo ek cout uw T Sys Arch Pattern Transfk Behavior System Architecture v ameet ch Augmentation Imported Model Status Current on Detets ma cs remove Import Control Transform Control import cai View Lo T Import Preference varo uen fene Import Status Inport nt running Figure 25 EDICT Replicate ADS Pattern Copyright 2011 Rockwell Collins Inc 30 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Apply the next pattern by pressing the Apply button This pattern replicates the Attitude Heading System AHS to create a redundant AHS function team core Fle Edt Navigate Search Project EDICT Run META Window Heb icis Qel Prle ri et Oe CY BR evict design SP AMO Resour
28. A Design Effort Design Option META Design Option System Architecture B Import D Augnertation Irported Model Status D Stak Problems Model Verfication 3 Error Log Model verification results are not avaiable Figure 14 EDICT Importing AADL Model into EDICT The current status of the model is stale since we ve created a new source instance model in AADL OSATE but have not yet imported it into EDICT To refresh the model in EDICT click on the Import button The Initial Avionics System model should now be imported into EDICT O Copyright 2011 Rockwell Collins Inc All rights reserved 19 GUIDED TOUR DEMONSTRATION OF THE TOOLS Hockwe A Collins 4 Applying Patterns to the Model In this section we will apply several design patterns to the Initial Avionics System imported into EDICT to make its design more tolerant to faults To begin first expand the tree in the EDICT Design Workspace window in the upper left corner of the screen until you can see the Initial to Final Avionics Architecture pattern transform as shown in Figure 15 Double click on this pattern to select it EDICT Design META Design Effort SysComp team core architecture patterns F e Edt Navigate Search Project EDICT Run META Window ILE Ja Pele ei tt or S EJ FE epicr Dega SP AACR L Resource FE toic Design Workspace Di Nd Design Effort META Design Effort Design Option META Design Option 5 NE
29. Architectures 2 Intia Avionics System 3 initial Aviorics System ME 3 System Architecture Aum 34 Architecture Traces c OU patterns e ss Arch Pattern Trans cmauvunenoeenew E A A E EA ASA owes wy WD Sys Arch Pattern Trask Behavior v Current View Dotas Import Control Import Preference varo Import Status NONE ext running Figure 31 EDICT Replicate Throttle Pattern O Copyright 2011 Rockwell Collins Inc 36 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Apply the last pattern by pressing the Apply button This pattern replicates the Fast Common Computing Module CCM in the IMA Platform team core Fle Edt Navigate Search Project EDICT Run META Window Heb ei ECAI eto Oe CY BR evict design gp AMO Resource Design Effort META Design Effort Design Option META Design Option Repkcate FGS Insert FGS Leader Selection Apply PALS bo PGS Leader Selection Insert Gabon Comenansd Selector Replicate Pitch Sensors Insert Pach Voter Replicate Arspeed Sensors Insert Airspeed Voter Beo ste ADS Replicate AHS Replicate PMS Rogie ote NAV il er Architecture Frameworks Sz META Aechkecture Frame S O Data Libraries YP Logical Architectures 8 BE System Architecture Trand ES System Architectures 2 Intia Avionics System 3 initial Aviorics System ME 3 System Architecture Aum 34 Architecture Traces c OU patterns e ss Arch Pattern Transft cmauvnenoeene
30. ES Design GAA Resurti E DICT Design workspace ll 2E E mra t Fes aiar e x n H Maren Por Piai d yiii Jac babet Design Eliot META Darin Effort Design Option META Design Option Capture the Current State of the System amp rchibecturmi s System Composition Se Comt Sf Laport Syelem RI uu idu ER AAN Hak Architecture Frameworks HE META Architecture Pramea E D Cute Libraries Logical Architectures p Saban Bachibosc unie Trans Patten lopy intial fovormcs Soest ees ra Erealie a New AADL Sys Lern Trisomie model i Gystem Architechures Erte or zelect Ehe parent folders ET inis Avions sys Iri Aaris Dyshem sel mr kogern u Fiia Aone yin ME EE Puktternopy Iris Avion c ln Ee ben sschibier bun ALERTS zt be mnia fsaonks System 13 architecture Traces partenmi 3 Sys ach Pattern Trah s nisl to Final Avionics T Gy Arch Parton Teach HS HETA Deuy EFF EO VF Behavior X L3 META Desun Effort Sys ndlyzer aj hel MET Demngn Effirt yscomp H uc Pagan Reci n cen Proj EE Outline ant 22 E E ws FDICT HA WTGAN 2 WAT Aeae System Architecture AAD Sytem Instance Mean Frei Bias Sym w lapot Do Haag abin mported Model Status Cunmont veneta F cta oen lap Cortina pest Eee Mont Import Prehererz Import Stats nport noc running H Pecblierirs r Mickel Yilin 52 GF Error Lig ELI Model werfication rendks are rot sealable Figure 40 EDICT Select Destination
31. ETA Design Option Repicate FGS Insert FGS Leader Selection Apply PALS bo PGS Leader Selection Insert Gabon Comenansd Selector Replicate Pitch Sensors Insert Pach Voter Replicate Arspeed Sensors Insert Airspeed Voter Beo ste ADS Replicate AHS Replicate PMS Rogie ote NAV Replicate PFD Repke ate Yoke Replicate Theottles Replicate Processor il er Architecture Frameworks Sz META Aechkecture Frame S O Data Libraries YP Logical Architectures 8 BE System Architecture Trand ES System Architectures 2 Intia Avionics System 3 initial Aviorics System ME 3 System Architecture Aum 34 Architecture Traces c OU patterns e ss Arch Pattern Transft cuson seeneow DOPOSIAL ceu T Sys Arch Pattern Tras Behavior v Current View Dotas Import Control Inert caca View Lo Import Preference Manus Import Status DONE Ant running Figure 27 EDICT Replicate FMS Pattern O Copyright 2011 Rockwell Collins Inc 32 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Apply the next pattern by pressing the Apply button This pattern replicates the Navigation System NAV to create a redundant NAV function team core Fle Edt Navigate Search Project EDICT Run META Window Heb icis ECAA t 07 CY BR evict design SP AMO Resource Design Effort META Design Effort Design Option META Design Option Repicate FGS Insert FGS Leader Selection Apply PALS bo P
32. FCS Hage Conte acm ADG A 5I reo Free CZ ru a w ney Bee D PCS NS E THO TRACT THPOT P TRPOT e FCG TRPOT vost VOKEA VOKE t ACS vORE dc c cT ce6eev6ee 6e9mSliuIiI lt z 4 aatia dl Avionics System impi BO hotel Pron 9 Tag W ervey C Seri E Pan x Ready Avionics Syrtem Impl ion 9 CaP NUM SCRL WAN Figure 45 SysML Redundant Avionics System O Copyright 2011 Rockwell Collins Inc 49 All rights reserved GUI DED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins 6 Verification of the Final Avionics System To simplify the demonstration we have provided a final version of the avionics system model This model was created in SysML by editing the exported model from the previous section to add hardware software bindings timing properties for threads and connections and any additional ports and connections that were not added automatically by the pattern transforms We have also added system level properties in the form of contracts that are appropriate for the fault tolerant version of the system The Final Avionics System model can be imported through the SysML translator using Final Avonics System eap or the pre translated AADL version can be imported directly To do this we must start by deleting the Initial Avionics System AADL model This is necessary since an EDICT OSATE workspace is a single namespace there would be conflicts if we attempted to loa
33. GS Leader Selection Insert Gabon Comenansd Selector Replicate Pitch Sensors Insert Pach Voter Replicate Arspeed Sensors Insert Airspeed Voter Beo ste ADS Replicate AHS Replicate PMS Rogie ote NAV Replicate PFD Repke ate Yoke Replicate Theottles Replicate Processor il er Architecture Frameworks Sz META Aechkecture Frame S O Data Libraries YP Logical Architectures 8 BE System Architecture Trand ES System Architectures 2 Intia Avionics System 3 initial Aviorics System ME 3 System Architecture Aum 34 Architecture Traces c OU patterns e ss Arch Pattern Transit cups on seeneow SPeredcecec ease eee gags cu oyu WP Sys Arch Pattern Trask Behavior v Current View Dotas Import Control Inert caca View Lo Import Preference varo Import Status DONE Ant running Figure 28 EDICT Replicate NAV Pattern O Copyright 2011 Rockwell Collins Inc 33 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Apply the next pattern by pressing the Apply button This pattern replicates the Primary Flight Display PFD to create redundant Primary Flight Display systems ws QS 9 ri rt Ge CY BR epicr Design saan Ls Resource Design Effort META Design Effort Design Option META Design Option Repkcate FGS Insert FGS Leader Selection Apply PALS bo PGS Leader Selection Insert Gabon Comenansd Selector Replicate Pitch Sensors Insert Pach Voter Replica
34. HE DATA OR THE LSE OR OTHER DEALINGS IN THE Bb property bi Comment DATA 13 META Design EWort SOC eimpeartedeackage gt bed Package 3 Le3 BETA Diay EArt oys nalyzer Het META Berge Elik irea X E wes ED ICT We acusa b com gt o Pg B occumedcystemType s System Type Complete Aois Synnem m E T T T 3 ie wwTG AADL TS PER uaau Problems C Properties Model Yerficetion E Console 2 3 m Pugn Bebsunes Loading Enterprise Archireer API Reading Packages Remding Dara Types Besding Data Implementations Rending System Tynes Re amp ding System Implementations Writing packages Uririmng component types cicing campanent implementations Uriring praperries riting imparted packages Uritirng max files Vririmng aadi files Done imparting madal PEELE E Importing model from ysNL opening Bepositorg CitDocuments and Dettings spmiller Desktopi HETA 11 PublichTools Distribution Finali Example Hodala Initial Avi Selected Object eoenedSystemimplement sion System Implementation Compete Arons System Dompete amp vionicr System impi Figure 12 EDICT Instantiating the Complete Avionics System Implementation Expand the TOP aaxl2 file displayed in the main window until you see the line for the implementation of the Complete Avionics System Click once on this line to select it and then select OSATE Instantiate system gt owned SystemImplementation Compl
35. ICT Core Tool Suite Licensed toc Evaluation by Steve Miller for Rockwell C 10j xj Pie Edt Navigate Search Project OSATE Analyses EDICT Run META Window Help e n A In xx 6 Ee 5 alos ewe S Gd ae ve e t EJ OKT Desg aane L Resource 1 AAO Navigekor ts 31 22 Ini to Pinel Avionks System 1 To 25 T name for Modified System Architecture PatternCcopy IRIS Aviones System ardheysmi Capture the Current State of the System Architecture se 8 E META Design Effcet SysAnalyzer Transform Instantisoon Seve Copy Problems ES Properties 7 Model Verification GJ Console 0 deri Descr Resource Path Location T Figure 41 META Generate AADL Textual Model Copyright 2011 Rockwell Collins Inc 45 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Hockwe r Collins The transformed model still requires some manual editing before it is complete While this can be done directly in OSATE on the textual AADL model it 1s easier to do this on the graphical SysML model To export the transformed AADL model to SysML select the Initial Avionics System model or Final Avionics System model if your renamed it and select the META Export SysML function from the main menu bar In the pop up window that appears navigate to and select the Avionics System After Pattern Application eap file in the Avionics System After Pattern_ Application folder in your Examples folder This will export a copy of the transformed model in
36. Ine ding r p Reading component implementations lOpening SysML repository C Decuments and Settings spmiller Desktop META II Public Tools Distribution Final Example Models Avionics System After Pattern Applic Figure 42 META Export AADL Model to SysML Normally the new features added by the pattern applications would be laid out using the default layout provided by Enterprise Architect To avoid the need for extensive editing in this exercise a layout file has already been created in placed in the directory for the Avionics System After Pattern Application The SysML export function will use this layout file to position the new features neatly O Copyright 2011 Rockwell Collins Inc 46 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins Navigate to the Avionics System After Pattern Application directory and double click on the Avionics System After Pattern Applicate eap file An Enterprise Architect window similar to that shown in Figure 43 should appear The transformed Avionics System model is in the Exported System model E Avionics System Alber Pattern Application EA Py i t d amp L 8E urn UR m uh n n zdtlaults z D H Es Eaix Hormal E gt File Edit view Project Disgram Element Tools Analyzer amp dd ins Setting Window Help Proj ect Browrer n 7 x S m a a DIE EE E Aonig Sysbem After Pattern fopleakion 3 OW L tan Page b Boss Li evene
37. L GC mds valid bool FGS L LSO leader int real real real real bool real bool real FGS L LSO valid bool FGS HR GC cmds pitch delta real FGS_R GC mds active bool FGS_R GC mds valid bool FGS_R LSO leader int FGS_R LSO valid bool leader_pitch_delta real Step O 4 486486 2 540541 0 0 TRUE 0 TRUE 4 486486 TRUE TRUE 2 TRUE 0 05405 FALSE FALSE 0 FALSE 0 1 3 540541 1 594595 4 432432 4 486486 TRUE 0 05405 FALSE 0 05405 FALSE FALSE 3 FALSE 0 67568 FALSE TRUE 1 TRUE 4 486486 2 2 594595 0 648649 0 054054 0 05405 FALSE 0 67568 FALSE 0 78378 FALSE TRUE 2 TRUE 0 7027 FALSE FALSE 0 FALSE 4 486486 3 1 648649 0 2973 0 108108 0 78378 FALSE 0 7027 FALSE 0 83784 FALSE FALSE 0 FALSE 0 72973 FALSE TRUE 1 TRUE 4 486486 4 1 189189 0 62162 4 432432 0 83 84 FALSE 0 72973 FALSE 0 89189 FALSE FALSE 3 FALSE 0 62162 TRUE TRUE 2 TRUE 4 486486 5 0 243243 0 27027 0 56757 0 89189 FALSE 0 62162 TRUE 0 054054 FALSE TRUE 2 TRUE 0 324324 FALSE FALSE 0 FALSE 0 62162 In this counterexample each FGS goes through cycles of valid and invalid so quickly that it never becomes active during steps 1 2 and 3 This allows an unacceptable pitch delta is accumulate just as in the previous counterexample 8 3 Increasing ADS Max Pitch Delta The Air Data System max pitch delta is 1 0 by default const ADS_MAX PITCH DEL
38. ORS OR a 4 Comment COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM DAMAGES OR OTHER LIABILITY 3 p Comment WHETHER IN AN ACTION OF CONTRACT TORT OR OTHERWISE ARISING FROM OUT 2 piss Comment OF OR IN CONNECTION WITH THE DATA OR THE USE OR OTHER DEALINGS IN THE 2 M Comment DATA 4 lt importedPackage gt Aadl Package gt importedPackage gt Aadl Package lt gt lt importedPackage gt Aadl Package 4 lt importedPackage gt Aadl Package gt lt importedPackage gt Aadl Package oo lt gt lt importedPackage gt Aadl Package gt lt importedPackage gt Aadl Package m lt gt lt importedPackage gt Aadl Package 2 A gt lt importedPackage gt Aadl Package eX lt gt lt importedPropertySet gt Property Set 4 cimportedPropertySet gt Property Set B4 a Control mem Figure 50 Selecting a System Implementation We run AGREE by selecting Verify with Kind from the META menu The results will be displayed in a new window within Eclipse The results for the Flight Control System Impl are shown in Figure 51 Here we see a successful run where all the system properties are verified O Copyright 2011 Rockwell Collins Inc 54 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins FCS aaxl2 cex7004467757879157162 xls Z3 Home Insert Page Layout Farmulas Data Review View Acrobat ie Property IResult 2 Assumptions for AP valid 3 Ass
39. S Insert FGS Leader Selection Apply PALS bo PGS Leader Selection Insert Gabon Comenansd Selector Replicate Pitch Sensors Insert Pach Voter Replicate Arspeed Sensors Insert Aurspeed Voter Beo ste ADS Replicate AHS Replicate PMS Regi ote NAV Replicate PFD Repke ate Yoke Replicate Theotties Replicate Processor E BY Architecture Frameworks Sz META Archkecture Frame ie Data Libraries YP Logical Architectures 5 E System Architecture Trandz i System Architectures 2 Intia Avionics System 3 initial Aviorics System ME 3 System Architecture Auge 34 Architecture Traces c OU patterns e ss Arch Pattern Transft initis to Final Avionics cuson seeneow e Sere eee RPP cua T Sys Arch Pattern Tras Behavior Imported Model Status v Current View Dotas Import Control Import Preference varo Import Status import vt runang Figure 22 EDICT Insert Pitch Voter Pattern O Copyright 2011 Rockwell Collins Inc 27 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Apply the next pattern by pressing the Apply button This pattern replicates two copies of the airspeed sensor in the Air Data System ADS to create a triply redundant sensor system team core architecture patterns transforms F e Edt Navise Search Project EDICT Run META Window Heb Iss Ga ee eek eto tip evict om SAM L Resource Replace FGS Insert FGS Leader Selection Apply PALS bo PGS
40. TA 1 0 If we increase this to 2 0 the following counterexample 1s generated O Copyright 2011 Rockwell Collins Inc All rights reserved 57 GUIDED TOUR DEMONSTRATION OF THE TOOLS Signal Type Step AD L pitch val real 4 AD R pitch val real 2 AP CSA csa pitch delta real AP GC L cmds pitch delta real AP GC L mds active bool TRUE AP GC HR cmds pitch delta real AP GC R mds active bool TRUE FGS L GC cmds pitch delta real 4 FGS L GC mds active bool TRUE FGS L GC mds valid bool TRUE FGS L LSO leader int FGS L LSO valid bool TRUE FGS HR GC cmds pitch delta real FGS_R GC mds active bool FALSE FGS_R GC mds valid bool FALSE FGS_R LSO leader int FGS_R LSO valid bool FALSE leader_pitch_delta real In step 0 the left FGS 1s active with a pitch value of 4 8 while the right FGS 1s inactive and has a pitch value of 2 9 within the 2 0 bound of the left FGS value In step 1 the right FGS is invalid 0 8 2 3 0 0 1 3 Tet 0 1 4 8 TRUE 3 FALSE 0 6 FALSE FALSE 3 FALSE 0 5 FALSE TRUE 1 TRUE 4 8 Hockwe 0 45 FALSE FALSE 0 FALSE 0 4 ns and becomes inactive while the right FGS remains inactive and its pitch value becomes 1 1 within the 2 0 bound of its previous value In step 2 the right FGS becomes active and its pitch value is 0 4 again within 2 0 of its previous value This pitch value is picked up by the autopilot system in step 3 which now sees a sudden jump fr
41. ader Selection Insert Galore Command Selector Replicate Pitch Sensors Insert Pach Voter Repicate Arspeed Sensors Insert Airspeed Voter Regie ate ADS Replicate AHS Repkcate PMS Regie ote NAY Replicate PFD Repke ate Yokes Replicate Throtties Replicate Processor i BY Architecture Frameworks Sz META Archtecture Frame e Data Litas 1 Logical Architectures 8 SE System Architecture Trand i9 System Architectures TF Intia Avionics System G uu 9 wv LIJ 2 121 1 12 12 4 14 4 3 initial Avionics System ME S System Architecture Auge 1 N o 4 Architecture Traces c S patterns amp T Sys Arch Pattern Transft n initial to Wh Sys Arch Pattern Trans Behavior ee t me ne eyna System Architecture v ameet cb Augmentation Imported Model Status Current View Detais Import Control Import Preference Manus Import Status DONE not running Figure 20 EDICT Insert Guidance Command Selector Pattern Copyright 2011 Rockwell Collins Inc 25 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Apply the next pattern by pressing the Apply button This pattern replicates two copies of the pitch sensor in the Air Data System ADS to create a triply redundant sensor system Tm P MAAIE Sura Peut MNT Mm EDU AA HM ws SQ 9 eto Oe til evict Design SP AME O Resource i Design Effort META Design Effort Replace FGS Insert FGS Lea
42. ce Design Effort META Design Effort Design Option META Design Option Repkcate FGS Insert FGS Leader Selection Apply PALS bo PGS Leader Selection Insert Gabon Comenansd Selector Replicate Pitch Sensors Insert Pach Voter Replicate Nrspeed Sensors Insert Airspeed Voter Beo ste ADS Replicate AHS Replicate PMS Rogie ote NAV Replicate PFD Repke ate Yoke Replicate Theottles Replicate Processor il er Architecture Frameworks Sz META Aechkecture Frame S O Data Libraries YP Logical Architectures 8 BE System Architecture Trand ES System Architectures 2 Intia Avionics System 3 initial Aviorics System ME 3 System Architecture Aun 34 Architecture Traces c OU patterns e ss Arch Pattern Transft cuson seeneow oh Oh oh oh 2 Se oe cua T Sys Arch Pattern Tras Behavior v Current View Dotas Import Control Inert caca View Lo Import Preference varo Import Status DONE Ant running Figure 26 EDICT Replicate AHS Pattern O Copyright 2011 Rockwell Collins Inc 31 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Apply the next pattern by pressing the Apply button This pattern replicates the Flight Management System FMS to create a redundant FMS function Jic DN E Fle Edt Navigate Search Project EDICT Run META Window Heb icis Qel Prle ri et Oe CY BR evict design SP AMO Resource Design Effort META Design Effort Design Option M
43. cture Traces c OU patterns e z Arch Pattern Transf cmaun seenew CS CCS AV gsgs cx Bw liti to T Sys Arch Pattern Transfk Behavior System Architecture v ameet cb Augmentation Imported Model Status v Current View Detais Import Control Import Preference varo Import Status Inport nt running Figure 33 EDICT Final Avionics System Copyright 2011 Rockwell Collins Inc 38 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS dem s ns EDICT provides an architecture browser view that allows us to see some of the other features that have been added by the pattern transforms We first need to save a copy of the transformed model Select the Save Copy tab towards the bottom of the Pattern Transform window This will display the screen shown in Figure 34 Enter the name you would like to save your copy under and click on the Save button The default name PatternCopy Initial Avionics System is fine S EDICT Design META Design Effort SysComp team core architecture patterns transforms Initial to Final Avionics System sysptml EDICI Core Tool File Edit Navigate Search Project EDICT Run META Window Help lw omelet laa eo E x EDICT Design AADL 0 Resource EJ EDICT Design Workspace El 1 i Initial to Final Avionics System 3 EL ts i Name for Modified System Architecture Design Effort META Design Effort 2atternCopy Initial Avionics Sys
44. d the models together Return to the AADL perspective and select the Initial Avionics System in the AADL Navigator pane on the left Then select Edit Delete from the menu bar In the dialog that appears be sure to check the box for Delete project contents on disk Now we can import the Final Avionics System model using the same procedure as in Section 3 The models are found in the Example Models Final Avionics System folder in the tool installation You can import either the SysML version or the AADL version In the next sections we will use the Lute and AGREE tools to verify different aspects of the final system design Copyright 2011 Rockwell Collins Inc 50 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Om ns 7 Using the Lute Structural Checker The Lute Structural Checker verifies user defined structural properties of AADL instance models Since one normally works with AADL declarative models the Lute checker is invoked by selecting an AADL system implementation which Lute will then instantiate to create an AADL instance model For example using the Final Avionics System we can open TOP aaxl2 and select the Complete Avionics System Impl as shown in Figure 46 e d2 27X ls TOP aaxl2 L1 El Fs platform resource Final Avionics System aaxl packages TOP aaxlz El 4 Aadl Package TOP El Public Package Section TOP l E Comment Copyright c 2011 Rockwell Collins Developed with the sponsorship
45. der Selection Apply PALS bo PGS Leader Selection Insert Gaadorce Command Selector Replicate Pitch Sensors Insert Pach Voter Replicate Arspeed Sensors Insert Aurspeed Voter Replicate ADS Replicate AHS Replicate PMS P epic ote NAV Replicate PFD Repke ste Yokes Replicate Theotties Replicate Processor ii ar Architecture Frameworks Sz META Archkecture Frame ie Data Lbs T Logical Architectures 8 BE System Architecture Tract i System Architectures 2 Intia Avionics System vo G uu 9 wv N PsPpSRPRPEPRPPEREREXXCC 3 initial Aviorics System ME 3 System Architecture Auge 34 Architecture Traces c O8 patterns eM ss Arch Pattern Transft e m o o cua T Sys Arch Pattern Trask Behavior System Architecture v ameet cb Augmentation Imported Model Status v Current View Dotas Import Control Import Preference Manus Import Status import vt runang Figure 21 EDICT Replicate Pitch Sensor Pattern O Copyright 2011 Rockwell Collins Inc 26 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Apply the next pattern by pressing the Apply button This pattern inserts a voter that selects the medial value of the three pitch sensors team core Fle Eat Navigate Search Project EDICT Run META Window Heb ei SQ 9 2 7 Or tif epicr oew shaa Resource i Design Effort META Design Effort Design Option META Design Option Replace FG
46. e 46 Selecting a System Implementation We run the Lute Structural Checker by selecting Run Built in Lute Theorems from the META menu The results will be displayed in the Eclipse console If the console is not visible it can be opened using Window Show View Other Console The results for the Complete Avionics System Impl are shown in Figure 47 Here we see a successful run where all the Lute theorems pass For each theorem a count of the number of checks executed 1s provided This count is useful for discovering when a theorem passes vacuously 1 e when 0 checks are performed O Copyright 2011 Rockwell Collins Inc 51 All rights reserved GUI DED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins E Problems 5 Properties El Console 3 gt BE Mi a E META Executing theorem PALS Period is Period Passed 2 check s Executing theorem PALS Group shares PALS Period Passed 4 check s Executing theorem PALS Causality Passed 2 check s Executing theorem PALS Period Passed 2 check s Executing theorem Not Collocated Passed 18 check s En Figure 47 Successful Results of Running Lute Built in Theorems We can break the Lute theorems by modifying properties on the model For example in TOP aadl we have the following line Actual Processor Binding gt reference HW B PRC applies to SW FCS FGS Rh If we change Hw B PRC to HW A PRC then the Not Collocated theorem
47. ete Avionics System Complete Avionics System Impl O Copyright 2011 Rockwell Collins Inc All rights reserved 17 GUIDED TOUR DEMONSTRATION OF THE TOOLS Hockvve f Collins Next display the EDICT Design perspective by clicking on the EDICT Design button in the upper left hand corner or by selecting Window Open Perspective Other EDICT Design from the menu bar The EDICT display should change to that shown in Figure 13 X EDICT Design EDICT Core Tool Suite Pie Edt Newgate Search Project EDICT Run META Window Heb 15 xj Q d M E kd CI BR epicr Design AMA Resource E EDICT Design Workspace er bE Design Effort META Design Effort Des gr 1 Option META Design Option v loxa D System Logical Architecture No Architecture Specified Problems Model Verfication 1 Error Log Model verification results ace not avaiable Figure 13 EDICT Displaying the EDICT Design Perspective O Copyright 2011 Rockwell Collins Inc 18 All rights reserved GUI DED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins Next click on the System tab on the tabbed window in the lower left of the screen to display the current status of the imported model as shown in Figure 14 X EDICT Design EDICT Core Tool Suite F e Edt Navigate Search Project EDICT Run META Window Heb 2 5 xj Q EY EB enicr Design ANA LO Resource ER EOT Design Workspace Je Hm Design Effort MET
48. etedsteerniersentnesseeneaeee 54 8 1 Removing Leader Selection Agreement sss mener 55 5 2 Allow me Immediate RELA ar eite eter etes eU her ap Cate bebe sen Eri ee i 56 5 9 Increasing ADS Max Pitch Delf scasesstebute t ient genie des ubetin to ade vis Uno EES 57 Copyright 2011 Rockwell Collins Inc 2 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rockiwe Collins List of Figures Figure 1 SysML Initial Avionics System Model ccccceseeeeeeeseeeeseeesessesssssessnsseneeeeens 6 Figure 2 SysML Initial Avionics System Top SW amp HW ceccccccscsccccccceeceeeeeeseeeeesseeetnnaeeees 7 Figure 3 SysML Initial Avionics System SW cccssssssssssssssssssssnccccecessccessessssssssssensenaaaaaes 8 Figure 4 SysML Flight Control System FCS sees 9 Figure 5 SysML Flight Guidance System FGS sssssseessssccccceccceeeeeseesessesssseceeceeeesseees 10 Figure 6 SysML Flight Guidance Process FGP eese 11 Figure 7 IMA Platform HW 1ossoe dose TUUI NUR EGET UM SIN SERUI ES IUUUN NUS EIU A UU Grete MENU EE UD M RES UNUEE 12 Figure 8 EDICT Displaying the AADL Perspective eee eene eene enne 14 Figure 9 EDICT Importing the Initial Avionics System SysML Model 15 IS c o een eee eee ee E eee ee re ee es 16 Pono I sears cts sass
49. ffort SysAnalyzer o gt META Dengi Effort SysComp i WSM EDXCT 8 13 WWTG AAK c WWTGReurces B Flugn Resources Problems C Properties 7 Model Verffication L2 Console C3 way ts Ean META Loading Enterprise Architect API al Importing mod from Jy75NL opening Repository i uments and Settings spmililer Desktop META II Pubiic Toois Distribution FinalV Example Nodels initial Avi Rea p E TEE ERR y vi 2229 nab5bnuz ee ee om M mM a z 1 ue n wv v 2202 o 202 oe 3 Uu m wor omoB mGmGmuc gcGmws 9 quo og 6G o uo og o0 O9 steve aoa um B8 34 is m u L a b C 6 c c6 cU m X ow On FH HH He RO S5 E p pa kA 9 po aJ et ad m 232 27 c0212 axso 8 n ewe OS 6 E M 5 A se a Figure 9 EDICT Importing the Initial Avionics System SysML Model Importing the SysML model will run Enterprise Architect in the background and may take several seconds Note that status messages indicating progress will be displayed in the console window as shown in Figure 9 2 If you do not have Enterprise Architect or the SysML AADL Translator installed you can import a pre translated AADL version of the model by selecting File Import and selecting the options for General Existing Projects Into Workspace as shown in Figure 10 Select the project root directory Example Models Initial Avionics System Initial Avionics System as shown in Figure 11 Be s
50. form window to undo all the pattern instances The EDICT display should appear similar to that shown in Figure 16 EDICT Design META Design Effort SysComp team core architecture patterns transforms F e Edt Newgate Search Project EDICT Run META Window es ar Jer jy ri et Oe Cy FR evict o SPAM Resource Rek ate FGS Insert FGS Leader Selection Apply PALS to PGS Leader Selection Insert Guadorce Command Selector Replicate Pitch Sensors Insert Patch Voter Replicate Arspeed Sensors Insert Airspeed Voter Brod ste ADS Replicate AHS Repkcabe PMS Regie ote NAV Replicate PFD Rep ste Yoke Replicate Throtties Repikcate Processor el E Architecture Frameworks az META Architecture Frames ie Data Libraries T Logical Architectures B System Architecture Transi 3 System Architectures TF Intia Avionics System 3 inia Aviorics System ME 3 System Architecture Auge 34 Architecture Traces c Y patterns a w y Arch Pattern Transf initial to T Sys Arch Pattern Trans Behavior e eio ojule LI 32 1 2 20 012 1 2012 123 21 21 2 w co ct o o eyna uyu System Architecture v ameet i Augmentation Imported Model Status v Current Figure 16 EDICT Reset Pattern Application to Initial System O Copyright 2011 Rockwell Collins Inc 21 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rocke Collins Apply the first pattern to the Initial Avionics System by clicking on the
51. g theorem PALS Group shares PALS Period lPassed 4 check s xecuting theorem PALS Causality Passed 2 check s xecuting theorem PALS Period Passed 2 check s Executing theorem Not Collocated Failed 31 gt SW FCS FGS L 32 gt SW FCS FGS R tl gt SW FCS FGS L FGP L35 t2 gt SW FCS FGS R FGP L35 Figure 48 A Failure of the Not Collocated Theorem Executing theorem PALS Period is Period Passed 2 check s Executing theorem PALS Group shares PALS Period Passed 4 check s Executing theorem PALS Causality Passed 2 check s Executing theorem PALS Period Failed 8 gt SW FCS FGS5 L FGP LS Executing theorem Not Collocated Passed 18 check z Eil A Figure 49 A Failure of the PALS Period Theorem Copyright 2011 Rockwell Collins Inc 53 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS OC ns 8 Using the AGREE Model Checking Tool The Assume Guarantee Reasoning Environment AGREE tool performs compositional reasoning over AADL models augmented with assumptions and guarantees The final avionics system model has been annotated so that the flight control system has all the assumptions and guarantees needed to verify its compositional correctness AGREE runs on an AADL system implementation That AADL system implementation must be selected when AGREE is invoked For example using the final avionics system we can open FCS aaxl2 and select t
52. he Flight Control System Impl as shown in Figure 50 El W platform resource Final Avionics System aaxl packages FCS aaxl2 El Aadi Package FCS El Public Package Section FCS Comment Copyright c 2011 Rockwell Collins Developed with the sponsorship 2 4 Comment of the Defense Advanced Research Projects Agency DARPA v 4 Comment we 4 Comment Permission is hereby granted free of charge to any person obtaining 3 Comment a copy of this data including any software or models in source or 2 un Comment binary form as well as any drawings specifications and i Comment documentation collectively the Data to deal in the Data without ad 4 Comment restriction including without limitation the rights to use copy 2 2n Comment modify merge publish distribute sublicense and or sell copies of 2 us Comment the Data and to permit persons to whom the Data is furnished to do 2 pei Comment so subject to the following conditions 4 Comment oe Comment The above copyright notice and this permission notice shall be 2 m Comment included in all copies or substantial portions of the Data Comment 3 aii Comment THE DATA IS PROVIDED AS IS WITHOUT WARRANTY OF ANY KIND EXPRESS OR n 4 Comment IMPLIED INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 2 pa Comment MERCHANTABILITY FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT 2 sut 4 Comment IN NO EVENT SHALL THE AUTHORS SPONSORS DEVELOPERS CONTRIBUT
53. ht Contrai Synem inp Fight Control System Fleght Comro System Plight Contra Syrtem ie E CaP NUM SCRL WAN Figure 4 SysML Flight Control System FCS The Flight Control System consists of a single Autopilot System AP a single Flight Guidance System FGS and a single Flight Crew Interface FCI The FCI processes the yoke and throttle inputs from the pilot Next we will review the internal structure of the Flight Guidance System FGS O Copyright 2011 Rockwell Collins Inc 9 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS oc T Navigate to and open the Flight Guidance System ibd as shown in Figure 5 System om X3 T M NE S i D e d A catur 8 E ad d esu noma 5 file Edit View Project Diagram Element Tools Anaiyter Add ins Settings Window Melp z Piar z wionics System g5885 Piget OGudanee System Impi UH Qo TOP Flight Owdahce Procert FERRER EHE i i B block Fight_Modes id block Fight Modes ingi fil bloc Guidance Commands S Mj block Guidance Commands 1moi ll bloc Guidance Dota S Mj block Guidance Data 1mol E block Lateral Modes m Mj block Lateral Modes Imo m Mj block Mode Loo iid block Moda Loge imel lg bloc Vertical Modes lg block Vertical Modes Imol amp e gj res E MA gi nay gj Pro nj meorne gj toe D rvses
54. icate FMS PatleEDsisonse ooo ras Drei A resp teen tina 32 Figure 28 EDICT Replicate NAV Pattern sse nennen eene nennen nennen eene eene eene 33 Figure 29 EDICT Replicate PED Paie errien an Eon re PY eee eo EXE dI e ea rudes or dioc 34 Copyright 2011 Rockwell Collins Inc 3 All rights reserved GUI DED TOUR DEMONSTRATION OF THE TOOLS Rockiwe Collins Fiore 30 EDICT Replicate Yoke Patteri serieren 35 Proure 31 EDICT Replicate Throttle Patlertiu eee comenta E E 36 Figure 32 EDICT Replicate Fast CCM Pattern esses eene eene eene eene enne 37 Figure 33 EDICT Final Avionics Syste einast en aE a E EEES E 38 Figure 34 EDICT Save Copy of Transformed Model seen 39 Figure 35 EDICT Open Architecture Browser ssssssssssseeeeeeeeen nennen nnns 40 Figure 36 EDICT Select Model for Architecture Browser seen 40 Figure 37 EDICT Properties Viewer in Architecture Browser sss 4 Figure 38 EDICT Export the Transformed Model to AADL ee 42 Figure 39 EDICT Select System Architecture to EXport ccccccccccccccccccccceceeeeeesssseseessssssaaaes 43 Figure 40 EDICT Select Destination for AADL System Instance essssseeeeeee 44 Figure 41 META Generate AADL Textual Model eese 45 Figure 42 META Export AADL Model to SysML esses 46 Figu
55. itecture Traces c OU patterns e ss Arch Pattern Transft T Sys Arch Pattern Trask Behavior v Current View Dotas Import Control Inert caca View Lo Import Preference Manus Import Status csmpson seeneow BORSA ceu Repkcate FGS Insert FGS Leader Selection Apply PALS bo PGS Leader Selection Insert Gabon Comenansd Selector Replicate Pitch Sensors Insert Pach Voter Replicate Nrspeed Sensors Insert Airspeed Voter Beo ste ADS Replicate AHS Replicate PMS Rogie ote NAV Replicate PFD Repke ate Yoke Replicate Theottles Replicate Processor Figure 30 EDICT Replicate Yoke Pattern O Copyright 2011 Rockwell Collins Inc All rights reserved 35 GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Apply the next pattern by pressing the Apply button This pattern replicates the Throttle subsystem to create redundant throttle control systems ws Q 9 4 eto OF til evict Design SP AME O Resource Design Effort META Design Effort Design Option META Design Option Repkcate FGS Insert FGS Leader Selection Apply PALS bo PGS Leader Selection Insert Gabon Comenansd Selector Replicate Pitch Sensors Insert Pach Voter Replicate Arspeed Sensors Insert Airspeed Voter Beo ste ADS Replicate AHS Replicate PMS Rogie ote NAV il er Architecture Frameworks Sz META Aechkecture Frame S O Data Libraries YP Logical Architectures 8 BE System Architecture Trand ES System
56. licate Arspeed Sensors Voter Insertion Insert Aurspeed Voter Repke ation Repke ste ADS Replication Replicate AHS Replication Replicate PMS Regie ation Beli ote NAV Replication Replicate PFO Regie tion Repke ste Yokes Regk ation Replicate Theottles Repikcation Replicate Processor equnew z LIJ 2 012 1 11 12 2 2 ULM 3 initial Avionics System ME 3 System Architecture Aug 12 Architecture Traces c Y patterns S P Sys Arch Pattern Transft w o ot o o N o eyna u inziato Final Avionics WP Sys Arch Pattern Trask Behavior System Architecture v ameet d Augmentation Imported Model Status v Current View Detats Import Control Import Preference Manus Import Status DONE y running Figure 19 EDICT Apply PALS to FGS Leader Selection Pattern O Copyright 2011 Rockwell Collins Inc 24 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rocke d Collins Apply the next pattern by pressing the Apply button This pattern inserts a Selector a type of voter in the Autopilot AP system so that the Autopilot only accepts Guidance Commands from the active FGS T Design META Design Cffort SysComp team core archtecture pattems transforms Initial to Final Avionics System sysptml DICT Core Tool Suite F e Edt Navigste Search Project EDICT Run META Window Help IN 1r gv 16 nui rto tif epicr design shaa Resource Rep ate FGS Insert FGS Leader Selection Apply PALS to PGS Le
57. nto AADL Import the model into EDICT Transform the model using architectural design patterns to add fault tolerance functionality Export the transformed model back to AADL Verify structural properties of the final version of the avionics system model using Lute Se eS oe YS Verify behavioral properties of the final model with assume guarantee reasoning using the AGREE tool 8 Understand the impact of changing the model by generating and viewing verification counterexamples produced by the AGREE tool Let s begin we hope you enjoy the tour Copyright 2011 Rockwell Collins Inc 5 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Hockwe A Collins 2 Reviewing the SysML Model If you have installed Enterprise Architect you can use it to review the Initial Avionics System SysML model that will be used in this example If you have not installed Enterprise Architect you should proceed to Section 3 where we describe how to import the AADL version of the model Start by making a working copy of the Example Models directory found in the distribution and double click on the Initial Avionics System eap file found in the Initial Avionics System directory This should open a screen similar to that shown in Figure 1 l2 Ra b ig g lt cetauir gt amp E Ad fj Basic Normal File Edit View Project Diagram Element Tools Anaiyter Add Ins Setting Window Help Toolbox B SAE serm IC CEET
58. om 4 8 to 0 4 which exceeds the 5 0 bound on pitch delta thus invalidating the system level guarantee The essential problem is that although the two sides are within 2 0 of each other and each side may change only 2 0 per step leader selection requires that there is one step where neither side is active while leadership is transferred Thus two changes of 2 0 may occur during this time leaving a total delta of up to 6 0 This does not occur when each side may only have a delta of 1 0 per step since then the total maximum delta is only 4 0 Copyright 2011 Rockwell Collins Inc All rights reserved 58
59. or System Architecture v Import D Augmentation Imported Moda Status v Current amona Import Control see s m Import Pref arene Maren Import Status Import M rung f Problems 77 Model venfication 2 O Error Log xj Model verfication results are not avalada Figure 38 EDICT Export the Transformed Model to AADL O Copyright 2011 Rockwell Collins Inc 42 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rockwel Collins A new pop up window will appear asking you to select the architectural model to export Select the name of the model you saved at the end of the pattern transform exercise E EDICT Design META Design Alart Syal omp team onre anheu jnatherns bransiorms Tnitial_bo Final Avienies Systemusyapind EDICT Cene Tanl Sis Pie Ed Mawigse Search Proiect EDICT Run META Window Helo ws Br F mE oet oe a AAD I Resource E EGICT Desin Workspace p ak Design Effort META Design Effort Design Option META Design Option Ys System Dompensition aF core BF Archibeckure Frameworks Be META dechbectune Frames gt y Cata Libraries x BE System Architecture Trance zi LF Stem Anchitiectures hama For Modified System Andichune Pattern Copy intial Aionies System archoyerl Capture the Currenk Saba of the Toprtem Pedicure Se m Enpnrt System Architecture Model to AADL system Architicture Michel Seiten Pica herus Srba Sechibezkbure sucked b
60. ow Help rere eet he ee eee E SysMIL Block Internal dg intis Avionics System m Part g 405 Gd Connector Part a ws mJ Distributed Pact rn cd Plow Part 5 gj cs cd Patidpaet Part gj rea G Signal s gj rc 3 Por p l res Wes 9 Port Mew gt pjm 9 Flow Specification 23 IMA 9 BAA Platform Mimpi ul block OOM Fat ysML Block Internal a Mj block CCM Faut Tei A A tad block CCM Siow E a Mj block CCM Slow Ingi E Profile ll block IMA_BUS E Profile B block 1MA BUS Jagi E A CCM Fast B block 1MA Dota 4p Stereotype id sblock IMA Potform G Metadass li block IMA Platform 1moi ij Enumeration la V Ea propertys A COM Fast B Common amp Gal property C COM Slow 3A Bb Gal peoperty IHA Bus IMA BUS B biok Poner 2S0Hhz nauc 3 Mj block PowerPC 250Mhz Impl Bj bod PowerPC 350Mhz 838 fe BUStoA BUS2C 3 Bj block PowerPC 350Mhz mpl IN rN B block Processor Memory B block Processor Memory mol v gj nay a Po IMA Bus IMA BUS gj rome 5 gl roe 5 gj tee m YOE 4 Ld EES a 4 SD stan Pace fib 45 M conet noni Sistem M uon Control System i Fight Guidance Sistem impi Fight Guidance Process impt BIMA Piattorm FP notes i Prop 9 Teg W Pros UE Seri Q Pan Oviput 3x M b M System Senet 7 Ls J 2 E Personal intormation Q Project Information Ready MA Platt et
61. ow Specification El SysML Block internal oA e f S block Complete Avioracs System E Profile m Profile ad sbilock Complete _Avioras_ System Impi Stereotype bp roper ty HW IHA Phorm FE Metadass Gal pecperty SW Avinries System ij Enumeration s gj res a gj vor aaasb ea e25u uenas 3 Pg zi ON D sat Pace M ab M Complete Avionics System BOB egt W o O Sen A han wm v 9 x M4 M System A Serot e OO MJ x bg Pertonal information O Project information Ready plete A te et Figure 2 SysML Initial Avionics System Top SW amp HW As shown in Figure 2 the Complete Avionics System consists of components for software SW Avionics System and hardware HW IMA Platform Next we will review the internal structure of the Avionics System SW component O Copyright 2011 Rockwell Collins Inc 7 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Navigate in the Project Browser to open the ibd for Avionics System as shown in Figure 3 This ibd is labeled AV and is located under the Avionics System Impl block in the AS package Bel P M 1 AL LA D ee dy X lt ctetauit 9g Ad Esie Normal E file Edit View Project Diagram Element Tools Anayter Addins Settings Window Melp E SysML Block Internal gy intis Avions System c3 Peet ig aos zb Connector Part zm Distributed Pact T g A 7 uf 2 c Plow Part 9
62. re 43 SysML Open Exported SysML Model 2 m tete rennen aero enr Lee ie 47 Figure 44 SysML Redundant Flight Control System ccceccscccccceeeseeessneneeeeeeeeeeseessneeeeeees 48 Figure 45 SysML Redundant Avionics System esses eene eene nnne 49 Figure 46 Selecting a System Implementation ccccsessessnnsceceeeeececeeeeessesesssssssnsssenaaaaes 5 Figure 47 Successful Results of Running Lute Built in Theorems sssssseeeeeeee 22 Figure 48 A Failure of the Not Collocated Theorem eeeseeeeeeeeeeeeeennns 53 Figure 49 A Failure of the PALS Period Theorem c ccessscccccceeeeseesesesesssesesseeensenecs 53 Figure 50 Selecting a System Implemoentattotn ueo cei etie eI eret eter eo eoe Ere tee SERERE aiea 54 Figure 51 Successful Results of Running AGREE 7 7 7 aterert ag oda ease su us cau ous 55 Copyright 2011 Rockwell Collins Inc 4 All rights reserved GUI DED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins 1 Overview The purpose of this Guided Tour is to provide evaluators and potential users of the Rockwell Collins META toolset with an overview of its capabilities It will lead you through a demonstration based on our Avionics System example to illustrate the functionality provided by each part of the toolset The tool framework consists of the following parts 1 Enterprise Architect
63. should fail To confirm this we make the described change and rebuild the AAXL files Note that every time we change AADL files we must explicitly tell OSATE EDICT to rebuild the corresponding AAXL files To do this from the Project menu select the Clean option choose Clean all projects and press OK We can then open TOP aaxl2 again select the Final Avonics System Impl and run the built in Lute theorems on it again This time the Not Collocated property fails as shown in Figure 48 The results show that the systems SW FCS FGS L and SW FCS FGS_R are declared as Not Collocated but they respectively contain the threads SW FCS FGS L FGP LS and SW FCS FGS R FGP LS which are bound to the same processor We can see another example of a Lute theorem failing by modifying timing information on the model To do this we look in FCS aadl and change the following line Latency gt 5 ms 8 ms applies to FGSLtoFGSR replacing the value of 8 with 10 Then we can rebuild the AAXL files using Project Clean again The results of running Lute on the modified model are shown in Figure 49 Here we see that the PALS Period property fails to hold for the thread SW FCS FGS L FGP LS O Copyright 2011 Rockwell Collins Inc 52 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins MELEE Iu Sole L IF AE META S OS Executing theorem FALS Period is Period Passed 2 check s Executin
64. t is configured with the necessary EDICT options and loaded with the design patterns we will be using in this exercise To load this workspace make sure the EDICT tool is not currently running Make a copy of the demo workspace folder found in the root directory of your EDICT installation and rename this folder workspace This will save the original version of the workspace in case you wish to do the guided tour demonstration on another occasion Lauch the EDICT tool If this is your first time to run EDICT you will need to enter your license key An evaluation license and key have been included with the distribution You will find the key in the file DARPA20110817 EdictLicenseKeys txt in the EDICT folder of the installation See the EDICT Core User s Guide and the EDICT AADL Adapter Guide for guidance on configuring EDICT Typically C Program Files re meta tools EDICT Copyright 2011 Rockwell Collins Inc 13 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins When prompted to select a workspace choose the workspace folder that you just created Be sure to select the workspace folder in the RC META TOOLS EDICT folder which may not be the default workspace suggested by the dialog This should result in a screen similar to that shown in Figure 8 of EDICT presenting the AADL perspective X AADL EDICT Core Tool Suite Licensed to Evaluation by Steve Miller for Rockwell Collins 5 xj F e Edt Newigs
65. te Nrspeed Sensors Insert Airspeed Voter Beo ste ADS Replicate AHS Replicate PMS Rogie ote NAV Replicate PFD Repke ste Yoke Replicate Theottles Replicate Processor il er Architecture Frameworks Sz META Aechkecture Frame S O Data Libraries YP Logical Architectures 8 BE System Architecture Trand ES System Architectures 2 Intia Avionics System vo G 4 9 wv 3 initial Aviorics System ME 3 System Architecture Auge 13 Architecture Traces c OU patterns e ss Arch Pattern Transft 72225272 BORA cu T Sys Arch Pattern Trask Behavior v Current View Dotas Import Control Inert caca View Lo Import Preference Manus Import Status DONE Ant running Figure 29 EDICT Replicate PFD Pattern O Copyright 2011 Rockwell Collins Inc 34 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS oer tollis Apply the next pattern by pressing the Apply button This pattern replicates the Yoke subsystem to create redundant yoke control systems Fle Edt Navis Search Project EDICT Run META Window Hep je IS 19 CY BR evict design gp AMO Resource Design Effort META Design Effort Design Option META Design Option ii er Architecture Frameworks Sz META Aechkecture Frame S O Data Libraries YP Logical Architectures 8 BE System Architecture Trand H S System Architectures EF Intia Avionics System 3 initial Aviorics System ME 3 System Architecture Aum 34 Arch
66. te Search Project OSATE Analyses EDICT Run META Window Help nggmjxxelHH JD jJejOor NS 5 G Q t1 E oT vespa AADL Resource e P AMD Nevigetor 3 D 5 led META Dengn Lffort 5OC ic META Design EllortSysAnahyrper y L2 META Design Effort 5v9Comp i WSM EDECT 2 WWTG AADK 8 le WWTGResources B Plugn Resources Problems Properties 7 Model Verfication L2 Console C3 Bg r 0 Nocomwmolestodepiy at this time p Figure 8 EDICT Displaying the AADL Perspective O Copyright 2011 Rockwell Collins Inc 14 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins There are two ways to import the Initial Avionics System into EDICT 1 If you have Enterprise Architect and the SysML AADL Translator installed import the Initial Avionics System SysML model by selecting META Import SysML from the menu bar at the top of the screen Use the Open file window that pops up to navigate to and select your copy of the Initial Avionics System eap file found the folder Example Models Initial Avionics System amp AADL COICT Core Tool Suite Licensed to Evaluation by Steve Miller for Rockwell Collins 5 xj F e Edt Navigate Search Project OSATE Analyses EDICT Run META Wow Help nnmHHlixxeemE I o ejoniweuijs5icg qes5 Qt Oy EJOT besgn gp Aare L Resource 42 ASA Nevigetor ES Sn zir Da Fe Inbal _Aviores System lc META Design Elfcet SOC L2 META Design E
67. tem archsysml Design Option META Design Option Capture the Current State of the System Architecture Save ES Initial Avionics System 4 Initial Avionics System System Architecture Auc 19 Architecture Traces CE d Patterns E n Arch Pattern Trar Initial to Final Avio b Outline Arch EST rd v Logical System vam Os System Architecture v Import s Augmenta 1 Imported Model Status v Current View Details Import Control Import cancel View Lo Import Preference Manua Import Status import nof running Transform Instantiation Save Copy fi Problems Model Verification 23 Error Log Model verification results are not available Figure 34 EDICT Save Copy of Transformed Model O Copyright 2011 Rockwell Collins Inc 39 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i A To open the architecture browser view select from the menu bar EDICT System Composer Open View Architecture Browser as shown in Figure 35 File Edit Navigate Search Project EDICT Run META Window Help mi a soc d Architecture Generation s ICT Desi IOI corr penes Ress De x i Architecture Browser 3 EDICT Design Workspace Report Manager Architecture Br r ta Workspace gt thitecture Pattern Transform Design Effort
68. to this EA repository providing status messages as shown in Figure 42 S AADL META Design Effort SysComp team core architecture patterns trensforms Intial to final Avionics System sysptral EDICT Core Tool Suite Licensed toc Evaluation by Steve Miller for Rockwell C o xj Pie Edt Nagste Search Project OSATE A syses EDICT Run META Window Heb oh Df BA xXxK BEBO ajOM Sal Ga a v e t Edu Dena Aare L Resource 42 AOL Navigator E 3 2 inti to Fins Avions System 23 E same for Modified System Architecture i Intal_Aviorks System Pattermcopy ARa Aviones System ardea e Capture the Current State of the System Architecture i padages Save ADS amt2 n A bout e PS e AS owd e C3 aaxl2 i FCI ami PS Pc i FG A Final Avionics System Dretan J final A cs Syster Ra FMS aaxt e IMA sx e NAY sacl 4 PFO en 4p THROTTLE sate TOP Complebe A M TOP cant 4 TYPES saxtz We YORE sat ic propertyset l META Deti Elficet SOC 3 META Deag Effcet SysAnabyrer Transform instantiation Seve Copy d E Problems C Properties 7 Model Verfication C Console 3 a51 g ri a0 8 13 wWTG AADE pus ES WWIGA xn jur ic ing packages m z M woe Writing component types mA Plugin Resources Writing component implementations Wricting properties vx iting imported packages lur iring anxl1 files Writing aadl files Done importing model Loading Enterprise Architect API Exporting model to SYSEL Reading packages
69. ult tolerance Next we will review the internal structure of the Flight Control System FCS Copyright 2011 Rockwell Collins Inc 8 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS oc T Collins Navigate to and open the ibd for the Flight Control System as shown in Figure 4 Initial Avionics System EA E l8l x mTpwEEIX DT E D RA RI derau E BEF emie Hamal z pue Edit View Project Diagram Element Toot Analyser addini Setting Window Melp Ed Connector Fart bd o Bittributed Part Ed Piom Part Ep Participant Past Spral M Per a Fo amp er EE m Few Specification Fifi u alors AD Bx DL Gl Sys Bock latarna 4E dessert AH Albiude Handing Date A 5A 5A ED osfkssBerl e CA Canl Surface Achse AED flePert 2 FD uidens Daka El Profile AE flow ert n FM Fl Management Daba P Profile o sfksePorl o MAY Nanigalion haba Ao skssPert e THROT Thio Data dh Sentotrpe 4j e owPerto YORE Yoho Dolto Cd Metaciass 4i ES property AP dustoplot System Lnumernation x Ep apenpestys FCT Flight _Crew_Interfiacn X E apeopentys Fad Fight Guidance Sysbem El Commen L dim B M FG af AB ae apn 4 55 5 amp ig ov amp B BAG a A kde 38 amp B THROTTLE A FA a me E roe B amp Bg Trees w gi voe 4 E BO Dhune G Prep Sp Tag i Prey LII Suri Vi Pan LED x ipa Sys eterna Basch Plig
70. umptions for FCI valid 4 Assumptions for FGS L X valid 5 Assumptions for FGS R valid 6 System level guarantees walid T 9 10 M 4 H Summary 13 7 Figure 51 Successful Results of Running AGREE In the subsections that follow we detail different ways of modifying the model so that AGREE reports a counterexample to the verification properties Each counterexample violates the system level guarantee that the pitch value reported by the autopilot must be within 5 0 units of its previous value In each case we highlight the most interesting parts of the counterexample manually and we sketch out the underlying reason why the property failed Note that the specifics of each counterexample may change from one run of AGREE to the next but validity or non validity will remain the same 8 1 Removing Leader Selection Agreement One fact about leader selection is that both sides will agree on the leader leader_agreement assert FGS L LSO Valid and FGS R LSO Valid gt FGS L LSO Leader FGS R LSO Leader If we remove this fact from FCS aadl rebuild the AAXL files and re run AGREE then the following follow counterexample is generated O Copyright 2011 Rockwell Collins Inc 55 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Hockwe Collins Signal Type Step 0 1 2 3 4 5 AD L pitch val real 4 8 3 866667 2 933333 2 1 066667 0 133333 AD R pitch val real 3 4 2 466667 1 533333
71. ure to check the box for Copy projects into workspace Copyright 2011 Rockwell Collins Inc 15 All rights reserved GUI DED TOUR DEMONSTRATION OF THE TOOLS Rockwe A Collins s C Import Select Create new projects From an archive File or directory Ele General i Archive File Ce File System El Preferences H E Plug in Development H E Run Debug H E Team HE XML 3 Import Import Projects Select a directory to search for existing Eclipse projects Figure 11 Copyright 2011 Rockwell Collins Inc 16 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS Rockwell Collins It is next necessary to instantiate the implementation of the Complete Avionics System First recompile the model by selecting Project Clean and selecting the Initial Avionics System model for cleaning Next expand the aaxl not the aad packages folder under the Initial Avionics System folder created when you imported the SysML model Double click on the file labeled TOP aaxl2 in the AADL Navigator window shown on the left of Figure 12 x ADL intial Avionics System aaxl packages TOP aaxlz EDICT Core Tool Suite F e Edt Navigate Seadh Project MATE Anayses DICT Run Aad odor META Window Heb Lr nn amp mHmi x xeaHMEIDO jwejevowmeujs5ips q jz eue Comment Copyright 6 2011 Rodkerell Coline Developed sth the sponsors iniia Avionice Systa de Cone dd Pe Deher dabra ral Ranch Prapta Agerscy DARPA
72. w S CN eee gags cx o ww T Sys Arch Pattern Trash Behavior v Current View Dotas Import Control Inert caca View Lo Import Preference varo Import Status DONE Ant running Figure 32 EDICT Replicate Fast CCM Pattern O Copyright 2011 Rockwell Collins Inc 37 All rights reserved GUIDED TOUR DEMONSTRATION OF THE TOOLS i Collins Your screen should now look similar to the one shown in Figure 33 This system includes redundant components with voters or selectors leader selection to ensure that only one side is active at a time and logical synchronization PALS of key components n META Design Cffort SysComp team core archtecture patterns transforms Initial to Final Avionics _System sysptmi DICT Core Tool Suite Pie Edt Navigate Search Project EDICT Run META Window Heb rw SQ 9 et Oe CY BR epicr begs S AMA CS Resource SD Design Effort META Design Effort Replace PGS Insect FGS Leader Selection Apply PALS to PGS Leader Selection Insert Gamdorkce Command Selector Replicate Pitch Sensors Insert Pach Voter Repicate Arspeed Sensors Insert Airspeed Voter Replicate ADS Replicate AHS Replicate PMS Regie ote NAV te Ed Architecture Frameworks Sz META Archkecture Frame ie Data Lirias 1 Logical Architectures 8 SE System Architecture Trand i9 System Architectures 2 Intia Avionics System 3 initial Avionics System ME 3 System Architecture Aug 13 Archite

Guided Tour

Contents

Download Pdf Manuals

Related Search

Related Contents