Engineering High-Assurance Software For Distributed Adaptive Real-Time .

Engineering HighAssurance Software forDistributed Adaptive RealTime SystemsSagar Chaki, Dionisio de Niz, Mark KleinSoftware Solutions Conference 2015November 16–18, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited

Copyright 2015 Carnegie Mellon UniversityThis material is based upon work funded and supported by the Department of Defense underContract No. FA8721-05-C-0003 with Carnegie Mellon University for the operation of the SoftwareEngineering Institute, a federally funded research and development center.Any opinions, findings and conclusions or recommendations expressed in this material are those ofthe author(s) and do not necessarily reflect the views of the United States Department of Defense.NO WARRANTY. THIS CARNEGIE MELLON UNIVERSITY AND SOFTWARE ENGINEERINGINSTITUTE MATERIAL IS FURNISHED ON AN “AS-IS” BASIS. CARNEGIE MELLON UNIVERSITYMAKES NO WARRANTIES OF ANY KIND, EITHER EXPRESSED OR IMPLIED, AS TO ANYMATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF FITNESS FOR PURPOSE ORMERCHANTABILITY, EXCLUSIVITY, OR RESULTS OBTAINED FROM USE OF THE MATERIAL.CARNEGIE MELLON UNIVERSITY DOES NOT MAKE ANY WARRANTY OF ANY KIND WITHRESPECT TO FREEDOM FROM PATENT, TRADEMARK, OR COPYRIGHT INFRINGEMENT.[Distribution Statement A] This material has been approved for public release and unlimiteddistribution. Please see Copyright notice for non-US Government use and distribution.This material may be reproduced in its entirety, without modification, and freely distributed in writtenor electronic form without requesting formal permission. Permission is required for any other use.Requests for permission should be directed to the Software Engineering Institute atpermission@sei.cmu.edu.DM-0003053Engineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited2

MotivationDistributed Adaptive Real-Time (DART) systems are key to manyareas of DoD capability (e.g., autonomous multi-UAS missions)with civilian benefits.However achieving high assurance DART software is very difficult Concurrency is inherently difficult to reason about. Uncertainty in the physical environment. Autonomous capability leads to unpredictable behavior. Assure both guaranteed and probabilistic properties. Verification results on models must be carried over to sourcecode.High assurance unachievable via testing or ad-hoc formalverificationGoal: Create a sound engineering approach for producing highassurance software for Distributed Adaptive Real-Time (DART)Engineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited3

DART Approach1. Enables compositional and requirementspecific verification1. ZSRM Schedulability (Timing)2. Use proactive self-adaptation and mixedcriticality to cope with uncertainty andchanging context3. Statistical Model Checking (Probabilistic)System Properties(AADL DMPL)Verification2. Software Model Checking (Functional)CodeGenerationBrings Assurance to Code1. Middleware for communication2. Scheduler for ZSRM3. Monitor for runtime assuranceDemonstrate on DoD-relevant modelproblem (DART prototype) Engaged stakeholders Nov 17, 2015 validityTechnical and operationalEngineering High-Assurance DART Software 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited4

Example: Self-Adaptive and Coordinated UAS onAdaptation: Formationchange (loose tight)Loose: fast but highleader exposureTight: slow but lowleader exposureChallenge: compute theprobability of reaching end ofmission in time while neverreducing protection to less than .LowHazardAreaChallenge: compare betweendifferent adaptation strategies.Solution: Statistical modelchecking (SMC)Engineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited5

Example: Self-Adaptive and Coordinated UAS onAdaptation: Formationchange (loose tight)Loose: fast but highleader exposureLowHazardAreaVideoTight: slow but lowleader exposureEngineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited6

Constrain the system structureand behavior to facilitate tractableanalysis and code generationCombine model checking& hybrid analysis toensure end-to-end CPScorrectnessFunctionalVerificationEnsures high-criticaltasks meet theirdeadlines despite tiveSelfAdaptationMADARAEfficient middlewareprovides distributedshared variables withwell-defined dataconsistencyProgram DART systemsand specify propertiesin a precise mannerStatisticalModelCheckingUse probabilistic modelchecker to repeatedlycompute optimaladaptation strategieswith bounded lookaheadEvaluate adaptationstrategy quality overmission lifetimeEngineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited7

Software for guaranteedrequirements, e.g., collisionavoidance protocol mustensure absence of collisionsHigh‐CriticalThreads (HCTs)Software for probabilisticrequirements, e.g., adaptive pathplanner to maximize area coveragewithin deadlineEnvironment– network,sensors,atmosphere,ground etc.Low‐CriticalThreads (LCTs)MADARA MiddlewareZSRM Mixed-Criticality SchedulerOS/HardwareBaked into theprogramminglanguages usedDistributedSharedMemorySensors &ActuatorsHCTLCTMADARASchedOS/HWDesign constraintenables analysistractabilityEngineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited8

System Architecture for eWaypointAdaptationManagerMADARA MiddlewareZSRM Mixed-Criticality RA MiddlewareZSRM SchedulerOS/HardwareEngineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited9

AADL : Architecture Analysis and Description LanguageDMPL : DART Modeling and Programming LanguageAADL : High level architecture threads real-time attributes Perform ZSRM schedulability via OSATE Plugin Generate appropriate DMPL annotationsDMPL : Behavior Roles : leader, protector Functions : mapped to real-time threads Period, priority, criticality (generated from AADL) C-style syntax. Invoke external libraries and components Functional properties (safety) : software model checking Probabilistic properties (expectation) : statistical model checkingAADL and DMPL supports the right level of abstraction atarchitecture and code level to formally reason about DART systems10Engineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited

https://github.com/cps-sei/dartDART Modeling and Programming Language (DMPL)Domain-Specific Language for DART programming and verifying C-like syntax Balances expressivity with precise semantics Supports formal assertions usable for model checking andprobabilistic model checking Physical and logical concurrency can be expressed in sufficientdetail to perform timing analysis Can invoke external libraries and components Generates C targeted at a variety of platformsDeveloped syntax, semantics, and compilerAADL and DMPL supports the right level of abstraction atarchitecture and code level to formally reason about DART systems11Engineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited

Proactive Self-Adaptationvia MAPE-KAnalyzeMonitorKnowledgeTarget systemPlanExecuteMAPE-K Emerged fromAutonomic ComputingCommunity[Kephart 2003]Engineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited12

Self-Adaptation in DARTSome aspects of the environment are unknown before the missionexecution for example, the threat level of different areas the environment conditions are discovered as the missionprogresses it’s not possible to plan everything in advanceNeed for proactive adaptation Adaptations may take time (e.g., formation change), so they have tobe started proactively Decisions taken at any point impact future outcomes (e.g., higherfuel consumption reduces range)Current solution based on constructing a MDP and using probabilisticmodel checking to find the best strategy at each adaptation point Exploring integration with Machine Learning techniquesEngineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited13

Adaptation using a Markov Decision ProcessHigh-level systemproperties relevant tocomputing objectivefunctionStochastic model of theenvironment updated atrun timeenvironmentTime over thedecision horizontactic1tick.clocktactic1 endtacticNsystemtacticN endself-adaptive systemStarting tactic or not is anondeterministic choicemoduleSystem model reflectseffect of tactic when tacticcompletesshared actionEngineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited14

t ct cPRISMstrategy synthesisResolvesnondeterministic choicesto maximize expectedvalue of objectivefunctiont 0T2t 1First choice independentof subsequentenvironment transitionsp1T1p2T1p3T2Ongoing work: replaceprobabilistic modelchecking with dynamicprogramming for speed.Engineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited15

Target relativeerrorDMPL Programwith random inputsProbabilistic Propertyencoded in DMPLEstimatedProbability that withrelative errorStatistical ModelCheckerProbability estimate for each property evaluated via “Bernoulli Trials”Number of trials required to estimate probability of a property depends on desired “relative error” (ratio of standard deviation to mean) true probability of the propertyRunning trials in parallel reduces required simulation time. SMC Client invokes Vrep simulation on each node. SMC Aggregator collects results and determines if precision is met. Simulations run in “batches” to prevent simulation time bias.Importance sampling (focuses simulation effort on faults)Statistical MC OverviewEngineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited16

ExecutableSMCAggregator(DMPL)dmplcLogGeneratorLog (1pernode)(DMPL)LogAnalyzerResultDMPLCompilerDART StatisticalMC WorkflowSMC ClientOneBernoulliTrialEngineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited17

Statistical Model Checkingof Distributed AdaptiveReal-Time Software. DavidKyle, Jeffery Hansen, SagarChaki. In Proc. of RuntimeVerifcation 2015Batch Log and eanalyzeSMC ClientSMC AggregatorUpdateacceptable?DART DistributedStatistical MCFuture Work: ImportanceSampling to reducenumber of simulationsneeded for “rare” events.andEach run of log-generator and loganalyzer occurs on a Virtual Machine.Multiple such VMs run in parallel onHPC platform. Clients can be added andremoved on-the-fly.Engineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited18

Statistical MC ingle ProtectorCoverageEngineering High-Assurance DART SoftwareNov 17, 2015 2015 Carnegie Mellon UniversityDistribution Statement A: Approved for Public Release;Distribution is Unlimited19