V&V Activities Within Two Brazilian Space Research Institutes

2y ago
30 Views
2 Downloads
2.21 MB
38 Pages
Last View : 22d ago
Last Download : 2m ago
Upload by : Maxine Vice
Transcription

V&V Activities within two Brazilian SpaceResearch InstitutesMiriam C. Bergue Alves*Valdivino Alexandre de Santiago Júnior Nandamudi L. Vijaykumar NASA IV&V WorkshopMorgantown, WVSeptember 11-13, 2012 NationalInstitute for Space Research - INPESão José dos Campos, SP, Brazil* Institute of Aeronautics and Space - IAESão José dos Campos, SP, Brazil

ObjectiveThis presentation relates some of the research initiatives ofthe Institute of Aeronautics and Space (IAE) and theNational Institute for Space Research (INPE) with respectto the use of formal methods for the improvement of theirV&V activities within the software development life cycle.NASA IV&V – Sept. 2012

Outline– Brazilian Space Program– Presentation of IAE– V&V Projects at IAE: Software Engineering Lab– Presentation of INPE– V&V Activities (Products/Projects) at INPE: CEA/LAC– ConclusionsNASA IV&V – Sept. 2012

Brazilian Space Program–Rocketry: launching and sounding rockets (IAE)–Space exploration: satellites (INPE)– Launch sites: Alcantara Launch Center andBarreira do Inferno Launch Center (DCTA)NASA IV&V – Sept. 2012

IAE’s Organization ChartDirectorR&D&I BoardR&H BoardombudsOffice of the DirectorInternal ControlCoord. Science andTechnology InformationAccident Prevention BoardIntelligenceSecurity BoardVice-DirectorProjects OfficeIAE 4 Sub-directorsAdministrativeAeronauticsSpaceSystems Eng.RadiologicProtectionDefenseSpace SystemsAtmospheric SciencesPropulsionIntegration & TestingElectronicSoftware Engineering Lab(LES)ChemistryMechanicsNASA IV&V – Sept. 2012

IAE’s Organization ChartDirectorR&D&I BoardR&H BoardOmbudsOffice of the DirectorInternal ControlCoord. Science andTechnology InformationAccident Prevention BoardIntelligenceSecurity BoardVice-DirectorProjects OfficeIAE 4 ms Eng.RadiologicProtectionDefenseSpace SystemsAtmospheric SciencesPropulsionIntegration & TestingElectronicsSoftware Engineering Lab(LES)ChemistryMechanicsNASA IV&V – Sept. 2012

V&V Projects at IAE Use of topology for verification of deadlocks inconcurrent systems– This project proposes a method that maps scenario-basedspecifications of concurrent systems, represented formally byMSCs (Message Sequence Charts), to a topological space. Thismapping allows to formally verify these specifications fordeadlock scenarios.– A simple “proof-of-concepts” prototype was constructed.NASA IV&V – Sept. 2012

V&V Projects at IAE Use of topology for lock(Pb)lock(Pa)unlock(Va)unlock(Vb)Progress graph oanalysis2unsafePbNASA IV&V – Sept. 2012

V&V Projects at IAE Use of statechart-assertions for requirements specification, validation and verification– Formal computer-aided validation and verification of critical timeconstrained requirements of the Brazilian Satellite Launcher flightsoftware. It included the entire specification, validation, and verification process based on UML statechart-assertions and log files.NASA IV&V – Sept. 2012

V&V Projects at IAE The SV&V processImport the log files into theSV&V environmentSystem requirements analysis/Reqs Specificationusing natural language (NL)StateRoverCreate a namespace mappingStateRoverRun the JUnit verificationtests against the assertions.Create UML statechartassertionsStateRoverValidate the statechartassertions using JUnitbased testingStateRoverExecute the resulting programon the VxWorks-based targetthereby creating log filesStateRoverAutomatically instrumentsource codeStateRoverBuild the instrumented versionof the system on the VxWorksbased targetNASA IV&V – Sept. 2012

V&V Projects at IAE SV&V – Some resultsValidation TestsVerification Tests220 tests (around 5 tests per assertion)4 log files (4 tests per assertion)220 JUnit classes - 1 JUnit class per test4 JUnit class- 1 JUnit class per log file132 success scenarios (around 60% ofthe scenarios)31 assertions passed in all tests (around70% of the assertions)88 scenarios expect an assertionfailure (around 40% of the scenarios)13 assertions failed at least in one test(around 30% of the assertions)NASA IV&V – Sept. 2012

V&V Projects at IAE Use of timed automata for model verification– A case study of a legacy space flight software system is beingconducted, where the flight control and the flight eventssequence chain of a satellite launcher are under study.– Use of model checking and a timed automata (TA) network tomodel the original requirements specification, incorporating newmission requirements and modifications.– Improve reliability in legacy systems evolution.NASA IV&V – Sept. 2012

V&V Projects at IAE Use of timed automata for model verificationD AE 6&AF&9. &6B86E 6& ?&9.&4 5:" *&;9. &!"# %&'( )* &,--./& ?@A 1 45&B6&&6C65 1&2 "2 8 6&; ? &C 6&- "2 5C&3 AE #&4"&012 "3 1 4567&)" )8"46&!NASA IV&V – Sept. 2012

V&V Projects at IAE Use of Event-B and Rodin Platform– The UML-B and Event-B language are being used for the modelselaboration of a case study that involves the control of the firststage of a launch vehicle, with the support of the computer-aidedtool Rodin Platform (Rigorous Open Development Environmentfor Complex Systems).– The work is at its initial phases of creating and refining themodels, with emphasis to the improvement of the systemdependability.NASA IV&V – Sept. 2012

V&V Projects at IAE!%/' 66(!"# %&',-*./#(0''!"# %&'()*& )"'93 B) /0'C"3(& #(."'*3& ) D'(.*'#23*:B-''/#00#* '.*2''A*()/9"3&3' 3 &0'235*30'!"# %&'()'*' ",-'./(481;''8*."-0#0'(.*' 3*3 .&3'*3 '0(3*. #)0';.B3&-'' 3 &0';) . 3';-0&3/'43 ?# 3/3*&0'093(#5(.:)*'1)23"#* '(.*' 3*3 .&3'#/9 )73/3*&0''.*2'() 3(:)*0'435*3/3*&'6 )7#* '9:9(8*."-0#0'8*."-0#0'@',30# *'@'A/9"3/3*&.:)*''NASA IV&V – Sept. 20128((39&.*(3'Event-B and Rodin Platform: the process()*& #E?&30'

V&V Projects at IAE Use of Event-B and Rodin Platform: exampleNASA IV&V – Sept. 2012

INPE’s Organization ChartINPE 7 Postgraduate programs.NASA IV&V – Sept. 2012

V&V Activities at INPE: Products Automated Test Case Generation based on Statecharts(GTSC):– Model-based test case generation based on Statecharts fourtest criteria (all-transitions, all-simple-paths, all-paths-k-C0configuration, all-paths-k-configurations) from the StatechartCoverage Criteria Family (SCCF);– Model-based test case generation based on FSM three testcriteria (DS, UIO, H-switch cover) where one (H-switch cover)is a new test criterion.NASA IV&V – Sept. 2012

GTSC 2.0: Main InterfaceNASA IV&V – Sept. 2012

V&V Activities at INPE: ProductsNASA IV&V – Sept. 2012

V&V Activities at INPE: Products SOLIMVA A methodology aiming at:– the generation of model-based system and acceptance testcases considering Natural Language (NL) requirementsdeliverables (artifacts) Version 1.0 (software testing);– the detection of incompleteness in software specifications Version 2.0 (software inspection with the aid of formalverification);– Formal Verification (Model Ckecking) of UML-based software Version 3.0 (Formal Verification in the traditional approach).NASA IV&V – Sept. 2012

The SOLIMVA methodology 1.0: WorkflowNASA IV&V – Sept. 2012

The SOLIMVA methodology 1.0: WorkflowSoftware Testing:- Model-Based Testing(Statechart-based testing; GTSC);- Combinatorial Designs;- Part Of Speech Tagging(SOLIMVA tool 1.0);- Word Sense Disambiguation(SOLIMVA tool 1.0).NASA IV&V – Sept. 2012

The SOLIMVA methodology 1.0: Tool (1.0)NASA IV&V – Sept. 2012

The SOLIMVA methodology 2.0: WorkflowSoftware Inspectionwith the aid of FormalVerification:- Model Checking;- Specification Patterns;- k-Permutations of n Valuesof Variables (Characteristics).NASA IV&V – Sept. 2012

The SOLIMVA methodology 3.0: WorkflowFormal Verification(UML)NASA IV&V – Sept. 2012

V&V Activities at INPE: Products Quality of Space Application Embedded Software – AutomatedSoftware Testing (QSEE-TAS): Automated test case execution,Automated test process documentation generation.NASA IV&V – Sept. 2012

V&V Activities at INPE: Applicationto Projects Alpha, Proton and Electron Monitoring Experiment inthe Magnetosphere (APEX).– Products GTSC, WEB-PerformCharts, QSEE-TAS. Quality of Space Application Embedded Software(QSEE) – Software for the Payload Data HandlingComputer (SWPDC).– Products GTSC, WEB-PerformCharts, SOLIMVA, QSEE-TAS. protoMIRAX Scientific Experiment (Balloonapplication).– Products GTSC, SOLIMVA.NASA IV&V – Sept. 2012

APEXIUT:-Command Recognition Component ofthe APEX embedded software;- Simulated version (Java).NASA IV&V – Sept. 2012

QSEE/SWPDC: Physical -232EPP H1(DataSimulation)(SWPDC)DAQADCEPP rTemperatureSimulationRS-232NASA IV&V – Sept. 2012Scientific InstrumentsIONEX

QSEE/SWPDC: Example of StatechartmodelSOLIMVA 1.0(methodology/tool)NASA IV&V – Sept. 2012

QSEE/SWPDC: Example of CTL propertiesand NuSMV model (SOLIMVA 2.0)NASA IV&V – Sept. 2012

QSEE/SWPDC: Remarks GTSC test suites with more than 300 test cases. SOLIMVA 1.0 better strategy with test objectivesclearly separated according to the directives ofCombinatorial Designs. SOLIMVA 1.0 Executable Test Cases predictedbehaviors that did not exist (Expert's strategy). SOLIMVA 2.0 362 CTL properties formalized, 21incompleteness defects detected.NASA IV&V – Sept. 2012

QSEE/SWPDC: Software DevelopmentLifecycleECSS gVerificationLevelsRequirementsand ArchitectureEngineeringDesign ependent Verification and ValidationFormalReviewsSRRPDRDDRCDRNASA IV&V – Sept. 2012QRAR

QSEE/SWPDC: IV&V Test Case Generation Model-Based Testing (FSM). Test Case Execution QSEE-TAS tool. Test Results Evaluation Four-step process:– Observation of test results (QSEE-TAS interface);– Assignment of a preliminary verdict;– Meeting (every week) IV&V team and customer representatives atINPE to evaluate the test reports;– Final verdict Non-Conformance Record (NCR).NASA IV&V – Sept. 2012

protoMIRAX Scientific ExperimentNASA IV&V – Sept. 2012

Conclusions Main V&V activities, products and projects in the area offormal V&V of safety-critical space software systems withinIAE-LES and INPE (CEA/LAC). More confidence in the right choice of techniques to be usedin each phase of development and in each part or componentof the space software. Importance of computer-aided tools to support the formalV&V process. Efforts to bridge the gap between the state of the art and thestate of the practice (application of research results to spaceprojects development).NASA IV&V – Sept. 2012

THANK YOU!Miriam C. Bergue Alves:miriammcba@iae.cta.brValdivino Alexandre de Santiago Júnior:http://www.cea.inpe.br/ valdivino/Nandamudi L. Vijaykumar:http://www.lac.inpe.br/ vijay/Welcome.htmlNASA IV&V – Sept. 2012

T1 a b T2 Pa Pb Deadlock unsafe 2 Pb T1 a b T2 lock(Pa) unlock(Vb) lock(Pb) unlock(Vb) unlock(Va) lock(Pb) . Alpha, Proton and Electron Monitoring Experiment in the Magnetosphere (APEX). . Reviews Processes Verification Levels NASA IV&V – Sept. 2012 ECSS Tailoring .

Related Documents:

4. 12 Meter (40') Drop Within Test 5. Fast Cook-Off Within Test 6. Slow Cook-Off Within Test 7. Bullet Impact Within Test 8. Fragment Impact Within Test 9. Sympathetic Detonation Within Test 10. Shaped Charge Jet Impact Within Test 11. Spall Impact Within Test 12. Specialty Within Test 13. Specialty Within Test 14. Specialty Within Test 15 .

Hour of Code—30 Activities for K-8 2 30 Hour of Code K-8 Activities Organized by Grade Kindergarten o Online activities o Misc. coding websites o Human robot o Human algorithm 1st Grade o Online activities o Misc. coding websites o Human robot o Human algorithm 2nd Grade o Online activities o Misc. coding websites o Sequencing o Animation 3rd Grade o Online activities

1. Colors - 16 activities 2. Numbers - 18 activities 3. Time - 36 activities 4. Weather - 17 activities 5. Food - 16 activities 6. Clothes - 23 activities 7. School Words - 20 activities Everyday English Everyday English Essential

systematic which engage employees through different activities. These employee engagement activities are classified into three different categories vis. 1) Learning activities, 2)Fun activities, 3)Creative leadership activities. In every category versatile activities are being implemented Statement of the problem

Chapter 5: Congruent Triangles 128 Enrichment Activities 151 Chapter 6: Relationships Within Triangles 153 Enrichment Activities 182 Chapter 7: Similarity and Trigonometry 189 Chapter 8: Circles 220 Enrichment Activities 244 Chapter 9: Polygons 248 Enrichment Activities 287 Chapter 10: Solids 293 Enrichment Activities 319 Chapter 11: Conics 326

Video/PowerPoint of Colors, Fonts, Infographics with Follow -up handouts and discussion. Ten activities, (Three activities on Colors, Four activities on Fonts, and Three activities on infographics) Resources-Two PowerPoints on Colors and Fonts/Typography; Two-word docs on 10 Points to Consider with Fonts and Using Infographics.

Activities These activities were developed with BRAC primary schools in mind but could be the basis for activities in any classroom where there is only one calculator. Each school will have one simple strong solar powered calculator and a set of activity sheets either in booklet form or printed on separate sheets. About the Materials The calculator activities are designed to: Help children .

activities to generalize sounds fiona balfe. speech pathologist 6 table of contents cont. level 2 descriptive games and activities cont. 2.6 jigsaw puzzle activities page 47 2.7 describing similarities and differences page 48 2.8 descriptive talks page 49 level 3 story activities page 50 3.1 simple story sequences page 51 3.2 complex story sequences page 52 3.3 picture sequence stories page 53