Safety assurance of an industrial robotic control system using hardware/software co-verification

Contents lists available atScienceDirect

Science of Computer Programming

www.elsevier.com/locate/scico

Safety assurance of an industrial robotic control system using hardware/software co-verification

Yvonne Murray

^a,∗

, Martin Sirevåg

^a

, Pedro Ribeiro

^b

, David A. Anisi

^a,c

, Morten Mossige

^d

aDept.ofMechatronics,FacultyofEngineeringandScience,UniversityofAgder(UiA),Norway bDept.ofComputerScience,UniversityofYork,UK

cRoboticsGroup,FacultyofScience&Technology,NorwegianUniversityofLifeSciences(NMBU),Norway dABBRobotics,Bryne,Norway

a rt i c l e i nf o a b s t ra c t

Articlehistory:

Received30April2021

Receivedinrevisedform17December2021 Accepted27December2021

Availableonline4January2022

Keywords:

Formalverification Co-verification Modelchecking Robots

Cyber-physicalsystems(CPS)

As a generaltrend in industrial robotics, an increasing number ofsafety functions are being developed or re-engineered to be handled in software rather than by physical hardware suchas safetyrelaysorinterlockcircuits.Thistrendreinforces theimportance ofsupplementingtraditional,input-basedtestingandqualityprocedureswhicharewidely used in industry today, with formal verification and model-checking methods. To this end, this paper focuses on a representative safety-critical system in an ABB industrial paint robot, namely the High-Voltage electrostatic Control system (HVC). The practical convergence of the high-voltage produced by the HVC, essential for safe operation, is formallyverifiedusinganovelandgeneralco-verificationframeworkwherehardwareand softwaremodelsarerelatedviaplatformmappings.Thisapproachenablesthepragmatic combinationofhighlydiverseandspecialisedtools.Thepaper’smaincontributionincludes detailsonhowhardwareabstraction andverification resultscanbetransferred between tools in order to verify system-level safety properties. It is noteworthy that the HVC application considered inthispaper has arather generic formofafeedback controller.

Hence, the co-verification framework and experiences reported here are also highly relevantforanycyber-physicalsystemtrackingasetpointreference.

©^{2021TheAuthor(s).PublishedbyElsevierB.V.Thisisanopenaccessarticleunderthe} CCBYlicense(http://creativecommons.org/licenses/by/4.0/).

1. Introduction

Theliberation ofindustrialrobotsfromtraditionalmetal cagesandsteadilyincreasingnumberofco-botsworkingside by side with humans are illustrative examples of a general trend in industrial robotics. In the wake of this, more and more safety-critical functions are now being developed to be handled by software and/or firmware componentsinstead of hardware safetyrelays or interlockcircuits. Modernindustrial robotsare heavily dependent on software-implemented safetysignalsto monitorandcontrol various criticalsubsystems suchascurrent/voltage supervisionandemergencystop orshortcircuitinterrupts.Thistrendbrings severaldistinctive advantagessuch ascost-reduction andincreasedflexibility.

*

Correspondingauthor.

E-mailaddresses:yvonne.murray@uia.no(Y. Murray),martin.sirevag@uia.no(M. Sirevåg),pedro.ribeiro@york.ac.uk(P. Ribeiro),david.anisi@nmbu.no (D.A. Anisi),morten.mossige@no.abb.com(M. Mossige).

https://doi.org/10.1016/j.scico.2021.102766

0167-6423/©^{2021TheAuthor(s).PublishedbyElsevierB.V.ThisisanopenaccessarticleundertheCCBYlicense} (http://creativecommons.org/licenses/by/4.0/).

Fig. 1.Inelectrostaticpainting,high-voltage(approximately40-90kV)chargesthepaintparticlesattheapplicator.Theparticlesfollowthelinesofthe electrostaticfieldfromtheapplicator(cathode)totheearthedworkpiece(anode).

Nevertheless,it alsointroduces orreinforcesnegativeside-effects, mostnotably inthe formofhighersystemcomplexity, vulnerabilityanddependability [1].

Tosetthestageforandaddressthisongoingindustrialtrend,thispaperadvocatesuseofformalverificationtechniques, whichcanprovideanextralevelofassurancebyverifyingthelogicofasystem.Theapplicationofformal methodsinthe robotics industry willideally helpto identifypotential pitfallsat amuch earlierphase ofthe development cycle [2] and serveasanimportantsupplementtothetraditionaltestingandsafetyrisk identificationandmitigationactionswhichare alreadyemployed [3].Obtainingsufficientlyhightestingcoverageincomplexindustrialsystemscanbetime-consumingand expensive.Inpractice,itismostoftennotviabletoaccountforeveryscenario,whichmeansthattestingcanfailtoreveal potentialsafety-criticalissues.

TheHVC systemconsidered inthispaperprovidesaperfectexampleofthis.Asdescribed in [4], apreviousversion of the HVCsoftware (SW)hasbeen showntocontain some errors,e.g., failure to properlyfollowthe givensetpoint. These errorsaredescribedinmoredetailin [4] andwentundetecteddespitepassingrigorousandcertifiedqualityassuranceand testingprocedures.Theseincludedaprioriandsystematicidentificationofriskmitigationplans(e.g.,usingHAZID/HAZOP), aswellasthoroughtestingproceduresconsistingofstaticcodeanalysis, unittesting,componenttestingandsystemtest I and II. Here,system test I encompasseshardware tests withthe IntegratedPainting System (IPS)and HVCactive, while systemtest IIentailstestingoftheentireroboticsystemusingactualpaint.

The robotic spray booth in, e.g., a car factory, may contain flammable solvent and paint particles in the air. Hence, paintrobotsarecertifiedforoperationinpotentially explosiveatmospheresinaccordancewithregionalATEX/NFPA/IECEx standards(ATEXDirective–2014/34/EU,IEC60079).ThepaintversionoftheABBIndustrialRobotControllerunit,denoted IRCP, is certifiedwith respectto theISO 10218 standard forsafetyrequirementsfor industrialrobots. Paintrobots using HVCarealsocertifiedaccordingtotheEN50176standardforusinghigh-voltageinexplosiveenvironments,whilethepaint atomiser iscertifiedinaccordancetoISO 9001andISO 14001.

Industrial paintrobots usehigh-voltage toperform electrostatic painting, whereparticles are electrically charged and attractedtothegroundedpaintobject,asseenin Fig.1[5,6].Inthisway,paintingqualityisensuredwhilepaintconsump- tionandcostsare minimised.However, theuseofhigh-voltage alsoposescertain risksofelectricshockandignition.Fire in thepainting cellmayresultin costlyproduction delays, aswell asdamageto theequipment. Therefore,itis ofgreat importancethattheHVCworksasintended.

TheHVCexampleillustratesthefactthatthecompleteeliminationofallerrorsismostoftennotpractical (duetocost and/ortime constraints)orevenpossible.Formalverificationprovidesusnotonlywithamathematicallysoundformalism for thespecification andverificationof robotic systemswhich ensures correctness, butalso provides evidencefor safety certification purposes. In fact,a survey onsafety-critical robot systems [1] recognisesformal verificationand correct-by- constructioncontrolsynthesisastwomainareasneededtodevelopsaferobotsystems.

Robotcontrolsystems,liketheHVC,haverathernaturalandgeneric propertiesthatare expectedtobefulfilledbyany feedbackcontrollertrackingasetpointreference.Formallyverifyingthatoverallthesetpointisfollowed,asystemproperty, however,requiresreasoningoverthecombined,time-dependentbehaviourofsoftwareandhardware.Forpragmaticreasons theseareoftenmodelledusingdiverselanguagesandformalisms,makingholisticreasoningchallenging.

Inspired by co-simulation approaches [7], in this paperwe propose a novel andgeneric co-verification approach for pragmaticverificationofsystemproperties.Modelsofthesoftwareandhardware arecoupledthroughplatformmappings that define how the inputsandoutputs of thesoftware are connectedto those ofthe hardware, interms ofits sensors andactuators. Withour approach, behaviouralproperties ofindividual models – that maybe established using separate domain-specifictools–can becombinedtosupporttheverificationofsystemproperties,usingpracticaltechniques,such asmodelchecking [8].

To illustrate the use of co-verification in a representative industrial case study, the HVC software is modelled in RoboChart [9–11], while thehardware is modelledin Simulink [12].RoboChart isa domain-specific language formodel- basedsoftwareengineeringofrobotics,withaformalsemanticsencompassingtimedandfunctionalaspects,thatistailored forformal verification.Simulink,on theotherhand,isadefactostandard forcontrol engineering,astypically usedinin-

dustryfordynamicsimulation.Forco-verificationweusetheMathWorksSimulinkDesignVerifier(SDV)toolbox [12],and theCSPmodel-checkerFDR [13],asintegratedintoRoboTool [9–11].

Importantly,wedemonstratethevalueofourapproachinidentifyingerrorsthatexistedinanearly-phaseHVCsoftware version asdescribedin [4].Inthenext phase,oncetheidentifiedsoftwareshortcomingshadbeenrectified,wewere able toshowthatitsatisfiesallsafetypropertiesofconcern.Namely,thatoverallthesystemtracksthehigh-voltagesetpointas setbyanoperator,andthatthesoftwareresetsthesetpointanddisablesthehigh-voltageifitsensesthatthepowersupply is unstable.This serves asa testimony of thestrength andsuitability of usingformal verificationmethods forindustrial safety-criticalsystems.

SomeinitialandpreliminaryresultsofourworkregardingformalverificationofHVCofindustrialpaintrobothavebeen previously published in [4]. Thispaper extendsthat work by addressing some fundamental and importantaspects, most notablyby:

1. takingintoaccountthetimedaspectsoftheHVCcontrollerusingthetimedsemanticsofRoboChart.

2. replacingthe simplified,binaryrepresentationofthe outputvoltagefollowingthesetpoint, witha realrepresentation andconsideringtimedanddynamicconvergencetowardsthesetpointsignal.

3. providinga crispdichotomybetweencontrol softwareandphysicalhardwareparts oftheHVCsystem, together with detailedplatformmappingin-between [14,15].

4. modellingthesystemdynamicsofthehardwareinSimulink [5,6].

5. usinganovelapproachtoco-verificationtocombinetheresultsfromhardwaresimulationsinSimulinkwiththemodel- checking capabilities of RoboTool [16] to verify that the high-voltage produced by the HVC follows the setpoint, a system-levelsafetyproperty.

The remainderofthispaperisstructuredasfollows.Section 2discussesrelatedwork.Section 3providesan overview ofthe HVCsystem, contains formulationsofthepropertiesto beformally verified(Section 3.1) andpresentsasimplified finitestate machine oftheHVC(Section3.2).Section 4constitutesthemain bodyof thecurrentpaper.Itdetails theco- verificationframeworkandexplainshowthestatemachinewasmodelledinRoboChartandcombinedwithMathworksSDV simulationandverificationresultsinordertoverifythesystem-levelsafetypropertyconcerningthehigh-voltage.Section5 reportson theverificationofsoftware properties.Finally, Section6provides some discussionandconclusions, aswell as suggestionsforfurtherresearch.

2. Relatedwork

Thesurveyonsafety-criticalrobotsystemsin [1] identifiessevenareasthatneedfurtherfocusandresearch inorderto develop safe, dependableroboticsystems. Itisnotable thatatleast fiveoftheseareasarerelevant inthecontext ofthis paper, namely:adaptive safetymonitoring, modelling and simulation forsafetyanalysis, formal methods forverification, correct-by-constructioncontrol,andcertification.

A recentsurvey [17] maps andlists thecurrent challenges, usedformalisms, tools,approaches, aswell aslimitations whenconsideringformalspecificationandverificationofautonomousroboticsystems.Themainresultsrevealthattemporal logic, state-transition andmodel checking are the main formalisms andapproaches used during the last decade. At the same time,the lackof appropriate toolsandsheer resistanceto adoptingformal verificationmethods inroboticsystems developmentarerecognisedasthemainlimitingfactorsforwiderimpact.Likewise,thelackofinteroperabilityandneedto capturetheessenceofcomplex,industrialroboticsystemsusingseveralformalismsandtoolsisrecognised.

Simulation plays an importantrole in thedevelopment of roboticsystems,and morewidely inthe domainof cyber- physical systems (CPS). However, current practice makes it difficult to soundly reason across models of the software, simulation, andhardware, which can exacerbate the reality gap.Co-simulation approaches [7,18] bridge the heterogene- ityoftools viaorchestration, forexample,usinga commonAPI asadvocatedinthe FMIstandard [19]. Besidesthe issue ofcodeportabilitybetweentools,roboticssimulators [20] tendtousedifferentphysicsengines.Arelatedapproach [15] to our workon co-verification,extendsthe diagrammaticsimulation language RoboSim[21] with facilitiesto coverphysical modellingofroboticsandestablishformallinksbetweensensors,actuators,andthesoftware,viaplatformmappings.

Kawaharaetal. [22] addresstheco-simulationofSimulinkandasubsetofSysML [23],wheredataisexchangedbetween models viainput/outputportsmodelledasS-FunctionsinSimulink.Theirfocusisontestingofsimulationsagainst timed constraintsexpressed viasequencediagramsusingthe UML-MARTE [24] profile.Cavalcanti etal. [18] give semanticstoa version ofINTO-SysML [25],aSysMLprofile suitableforco-simulationusingFMI,whereRoboChartisusedwithSimulink in theco-simulation ofa chemical detectorrobot. Bernardeschietal. [26] usetimed automata,encodedforreasoning in the PVStheorem prover [27], inco-simulation with aSimulink modelof acardiac pacemaker.Our focus,however,is on (co-)verification.

Recognisingthebroadrangeofaspectsintheengineeringofrobots,theuseofspecialised,andcomplementary,verifica- tiontechniquesiswidelyreportedintheliterature.Websteretal. [28] proposea“corroborative”approachwhereagreement issoughtbetweendifferentverificationtechniqueswithrespecttofunctionalrequirements,includingmodelcheckingwith PRISM [29],simulation-basedtestinganduservalidation.

Fig. 2.Block diagram of one part of the paint robot, containing the HVC.

Cardoso etal. [30] use differentmethodstoverifycomponents ofasimulation ofNASA’sCuriosityrover, wherehigh- level control is drivenby aBeliefs-Desires-Intentions (BDI) agent. The agent isverified using theAgent Java Path Finder (AJPF)modelchecker [31],whileitsinterfacewiththeenvironmentisverifiedusingDafny [32].FDRisusedtoverifyaCSP modeloftheactionlibrarynodesthat implementcontrol methodsfollowingthepublish-subscribeparadigm oftheRobot OperatingSystem(ROS) [33].Theemphasisisonverificationofcomponentswithformalmodelsguidingthegenerationof runtimemonitors.

Related, Bourbouhetal. [34] report onthe combineduseof severalmethodsandtools inthe development ofan as- surancecaseforaninspection rover,whichismodelledinAADL [35],SimulinkandEvent-B [36].Functionalrequirements are statedusing the structured natural language accepted by FRET [37], with semantics given in Linear Temporal Logic (LTL)suitableforanalysiswithLustre [38] modelsgeneratedfromSimulinkviaCoCoSim [39],aframeworkfordesign,code generation andanalysisofdiscrete dataflowmodels. Simulinkblocksmodellingtherover architectureare annotatedwith assume-guaranteecontractsbasedoncomponentrequirementsformalisedinFRET.System-levelpropertiesarethenverified viamodelcheckingwithKind2 [40],whilesomecomponentsareverifiedusingEvent-Binstead.

The literature is rich in approaches for formal verification of Simulink models. Reicherdt and Glesner [41] propose translating discrete-time Simulink models into Boogie [42] for verifying the absence of common error classes, such as overflows,underflows,division-by-zeroandrangeviolations.CoCoSimfollowsonfromprevious work [43] targetingLustre andSCADE [44]. Boström andWiik [45] propose a compositional approach forverifying Simulink blocks annotatedwith assume-guaranteecontracts.

Applicationsofformal verificationmethodologieswithin thecontrolandCPS communityhavemainly adoptedthehy- bridsystemandautomataframework ofAluretal. [46,47].Inthissetting,finite- andinfinite-timereachabilityconstitute the mainverificationtools, butunfortunatelyturnout to be anundecidable problemin general, leavingconservativeset approximation asthe only viableapproach [48,49]. Hybridautomata also assumeshaving infiniteaccuracy andinstanta- neousreactionwhichservesasanoticeablediscrepancytotherealsystemandimplementation;potentiallyinvalidatingthe verificationresults [50].

Focusingonformal verificationofindustrialrobotapplications,in [3],industrialrobot- andPLC-programsarecompiled intoPROMELAmodelsasinputfortheSPINmodelchecker [51].TheworkishoweverrestrictedtoLTLformulas.Itfurther differs fromourwork by solelyconsidering deadlocks, collisions andkill-switchviolations.Narrowingdown toindustrial paintrobots, [52] considersformalverificationofpaintsprayingusingtheARIADNEtoolforreachabilityanalysis.Thefocus hereissolelyonparametricdesignverification.

3. High-voltagecontrol(HVC)

Asimplifiedblock diagramoftheHVCpartofthepaintrobot canbeseen in Fig.2.TheHVC modulerunsthecontrol softwareloopsandassociatedcontrollogic.Here,ther(t)=^{H V}_Set P ointsignalisafunctionoftime,t,andusedasapriori given referenceforthe desired voltagelevel on the HVC,while the 24 V power signal provides the HVC withelectrical power. The u(t)=P W M_O utput signal serves as input signal to the Pulse Width Modulation (PWM) hardware. It is a percentage, from 0to 100%, mappedto an analog 0 to10 voltagesignal, which isthen increased inthe transformer.In the Cockcroft–Walton(CW) cascadegenerator, thereare severalvoltagedoublingcircuits, andthevoltageis rectifiedand furtherincreased,beforearrivingtotheapplicator,see Fig.3.Finally, y¯(t)= [^{I M};^{H V_Actual}]^{T denotecurrentandvoltage}

Fig. 3.The cascade modelled in Simulink with Simscape components, with the transformer, resistors and the Cockroft Walton voltage multiplier circuit.

Fig. 4.Setup for experimental testing with paint using ABB robot. Photo courtesy ABB, from [5].

measurements, respectively, whichare fed backinto theHVC.It isfurther noticeablethat froma paintrobot application point of view,it is giventhat HV_SetPoint∈⁰∪ [³⁰⁹⁰]^{, kV, that is,once the} high-voltage is activatedand turned on,it requires valueslargerthan 30kV, andthat ther(t)=HV_SetPointreferencevalue doesnot changevery often,andnever fasterthanwithin10secondsfromthepreviouschange.Thesefactswillbeusedsubsequentlyinordertoformallycapture andverifysomebasicpropertiesforHVC.

Following the lineof thought in [14,15], in order to distinguish anddescribe both the control software and physical hardwarecomponentsoftheHVCsystem,afaithfulmodelofthePWMhardwareisneeded.ThePWMhardwarecomprises thecomponentsinsidethedashedblueboxin Fig.2,thatis,thetransformer,CWcascadeblockandresistors.Fig.3depicts thediodes,capacitorsandresistorsdefiningaCWcascadeblockasmodelledinSimulinkSimscape,whichallowsmodelling ofphysicalcomponentsandsystems.Itisnoteworthy thatby design,eachsection oftheCWblockwill doubletheinput voltage sothat theoutput voltageofa CWcascadewith N sectionswillequal 2N V_in.The Simulink modelsused inthis workarebasedonandextractedfromexperimentallaboratorytestsperformedin [5,6] onrealABBpaintrobotsasdepicted in Figs.4and5.Thisservesasaback-dropandstartingpointforourwork.

ThepaintrobotHVCapplicationhassomefurtherdistinguishablestructureanddynamicsthatwillneedtobeconsidered andincorporatedintoourformalverificationscheme.Asdetailedin [5,6],thePWMhardwaremodelandcascadecontroller arebasedonthreedistinctmodesasgraphicallyillustratedin Fig.6:

•^{Charge:when a newexternal setpoint,} HV_SetPoint(t),withhigher value than thecurrentone arrives and thePWM hardwareisrampingupthecontrolsignal,u(t)=P W M_O utput(t),inordertoincreasethevalueofHV_Actual(t).

•^Running(steady-state):whenHV_ActualhasconvergedtoHV_SetPointandreachedasteadystate.

•^{Discharge:whentheexternal}HV_SetPointissettoalowervalueandPWM hardwareisdischargingsothatHV_Actual convergestoHV_SetPoint.

Fig. 5.Schematic overview of the lab setup for testing ABB paint robot. Photo courtesy ABB, from [5].

Fig. 6.TheHVChardwareandcontrollerhasthreedistinctmodes:Charge,Running(steady-state)and Discharge.TheIntegratedPaintingSystem(IPS) parametersRampLimitandTauPeriod provideupperlimitsonthe durationoftheCharge andDischargemodesrespectively. (Forinterpretationofthe coloursinthefigure(s),thereaderisreferredtothewebversionofthisarticle.)

Itisfurthernoticeablethatbydesign [53],thereareadditionallimitsonpeakdeviationbetweenHV_ActualandHV_Set- Point aswell asthe time duration of the Charge and Discharge modes. Namely, a parameter RampLimit determines the maximumtimeinsecondsthatitwilltake torampupthehigh-voltagefromminimumtomaximumlevel,i.e., from0 to 90 (kV).ThedefaultvalueofRampLimitis2 seconds.Likewise,itisknownthatitwilltakeTauPeriodsecondsforHV_Actual toreachalevelof30% aboveanewlowerHV_SetPointvalue.ThedefaultvalueofTauPeriodis3 seconds.Additionally,there aremaximumallowedoverandundervoltagelimits.Asmentionedearlier,theHVCapplication,onceactivatedandturned on,requireshigh-voltagevalueslargerthan30kV, sothatHV_SetPoint∈⁰∪ [³⁰⁹⁰]^kV.Consequently,theaforementioned limitsareonlyspecifiedat30 and90kV andover/underlimitsatothervoltagelevelscanbecalculatedusingsimplelinear interpolationbetweenthesevalues.Alloftheseparametersareusedforsafetysupervisionpurposesandarehencesetina conservativemanner.Inthenextsection,theseparameterswillbeusedtoformulateandlaterformallyverifythepractical convergencepropertyoftheHVCcontrollertoanewhigh-voltagesetpoint.

3.1. Propertiesforformalverification

Inthissection, thesetoffourpropertiesthatare tobe formallyverifiedis presented.Recognising thattheHVC hasa rathergenericformofafeedbackcontroller,itisnotablethatmostofthepropertiesinthissectionarerathernaturaland genericpropertiestobefulfilledbyanyfeedbackcontrollertrackingasetpointreference.

PropertyP1.Tostartwith,itisnaturaltorequirethatthemeasuredprocessvalue,whichinthecaseoftheHVCisdependent on time,t,anddenotedy(t)=HV_Actual(t),should convergetothe reference- or setpointvalue, r(t)=HV_SetPoint(t).To formalise this, itisnotedthat bothvoltagesignalsare non-negativetime-seriesandthatconvergence maybe definedby setting

e

(

t

) = |

^r

(

t

) −

^y

(

t

) | = |

HV_SetPoint

(

t

) −

^HV_Actual

(

t

) | ,

(1) andequivalentlyconsidering(asymptotic)Lyapunovstabilityoftheerrorterm,e(t),toorigin.

TakingtheparticularstructureanddynamicsoftheHVCapplicationasdiscussedpreviously intoaccount, thissetpoint convergencepropertycaninpracticebedecomposedintoconsideringa10secondtime-intervaldirectlyafteranewsetpoint arrives, within which practicalconvergence of HV_Actual to a narrow interval centred aroundthe new external setpoint (HV_SetPoint)canbeshown.ToeasethenotationandprovidesymmetrybetweentheCharge/Dischargemodes,let

τ ₌ τ

₀

₊

max

(

RampLimit

,

T au P eriod

),

(2)

where

τ

0 denotes thetime instance whena newsetpoint arrives. Also conservatively, set the peak deviationfrom new HV_SetPointas30% ofthesetpointvalue.Thewidthofthisnarrowinterval,aswellasschematictimechangesandevolution ofHV_SetPointandHV_Actualaredepictedin Fig.6.

Thissystem-levelpropertyinvolvesbothhardwareandsoftwarecomponentsandcanbeformallyspecifiedasfollows:

P1: Practicalconvergenceoftheactualsystemvoltage,HV_Actual,totheexternalsetpoint,HV_SetPoint:

∀

^t

≥ τ =⇒

^e

(

t

) <

0

.

3

×

^max

(

HV_SetPoint

(

t

),

1

).

PropertyP2-P3. To avoid residual effects and windup behaviours in the HVC, it is also reasonable to verify that both PWM_Output andthesoftwareinternal representationofHV_SetPoint,denoted mSetPoint,are setto 0 wheneverthe24 V power signal,andthereby theHVC-module,is switchedoff.Here,mSetPoint is distinguishedfromHV_SetPoint whichisa softwareextrinsicsignalsetaprioribyahumanoperatororapplicationengineer.

Thesetwopropertiescanbeformulatedasfollows:

P2: ThatPWM_Outputissetto0 wheneverthe24 V powersignalisoff:

24V_P ower

=

⁰

=⇒

^{P W M_O utput}

=

⁰

P3: ThatmSetPoint issetto0whenthe24 V powersignalisswitchedoff:

24V_P ower

=

⁰

=⇒

mSet P oint

=

⁰

PropertyP4.Finally,inordertoincrease theconfidenceinthecorrectnessofthemodel,itis customarytoverifythatthe HVCstatemachineisnotabletogointodeadlock.

P4: ThattheHVCsoftwareisnotabletogointodeadlock.

ThesearethefourpropertiesthatcollectivelyneedtobeformallyverifiedfortheHVCapplication.System-levelproperty P1 isverifiedusingourco-verificationapproach,whichisthesubjectof Section4,whiletheverificationofpropertiesP2- P4,that onlyconcernthesoftware,isdiscussedin Section5.Nextwepresentan overviewoftheoverallbehaviourofthe HVCsoftware.

3.2. Finitestatemachineoverview

InordertoperformmodelcheckingontheHVC,itsfunctionalitiesweremodelledasafinitestatemachine.Thissection presentsthe generalfinitestate machine asdepictedin Fig.7.This high-levelstate machine was givenby ABBandthen furtherdetailedandmodelledinRoboTool.Thisisthetopicof Section4.2.2.

Inthe state GateDriverRamping,whichisthe statethat theHVC firstenters whenitis switchedon,thePWM duty- cycleisrampedupgraduallytoensurestabilityandgradualincreasingofcurrentandvoltage.Then,intheInitialization state,initialparametersareset,aswellasupperandlowerlimitsforthehigh-voltage.

After the GateDriverRamping and Initialization steps are successfully finished, the state machine enters the Wait24VPower state. Whenthe HVChas24 V powerswitched onandis stable,the systementers theClosedLoopstate.

Thisistheidealstateforoperation,andiswherethecontrollerisregulating thevoltageinrelationtothesetpoint.Ifthe voltagebreachestheupperorlowerlimits,thestatemachinemovesfromClosedLooptoErrorMode.

ThereisalsoapossibilitytoenterErrorModefromtheClosedLoopandWait24VPowerstates,ifcertainvariablesareset oranywatchdogsorinterruptsaretriggered.Forinstance,aninterruptistriggeredifthesupplyvoltageisbelowacertain threshold,andanotheristriggeredifHV_Actualisaboveorbelowtheupperandlower limits,respectively.Gettingout of ErrorModerequiresmanualacknowledgementoftheoccurrederrors.

Fig. 7.Finitestatediagramofthehigh-voltageController(HVC),showingitsstatesandtheconditionsfortransitioningbetweenthem.TheClosedLoop stateistheidealstateforoperation,andiswherethecontrollerisregulatingthevoltageinrelationtothesetpoint.

4. Hardware/softwareco-verification

To reason about system properties, such as Property P1, it is necessary to consider the behaviour of both software andhardware.We proposea novelapproach,wherepropertiesareestablishedby co-verificationofmodelsconnectedvia platformmappingsthatrelatetheinputsandoutputsofsoftwareandhardware,viasensorsandactuators.Providingacrisp andsystematicseparationbetweenhardwareandsoftwarehassomedistinctadvantages.Tostartwith,withthisapproach, behavioural propertiesofindividual models– that maybeestablished usingdomain-specific tools–can be combinedto supporttheverificationofsystemproperties.Also,ourapproachenablesexplicitrecordingandcapturingofalldependencies andrelationsbetweenhardware andsoftware,which,whenneglected,areimplicitlyassumedtobetheidentity mapping.

Further,andaspreviouslymentioned,theongoingindustrialtrendismovinganincreasingnumberofsafetyfunctionsfrom physicalhardwaretosoftwareimplementation.Still,thereliability,dependabilityandtrustlevelsareverydifferentbetween hardware andsoftwarecomponentsinanindustrialroboticsystem.Thisframeworkhencesetsthestageformorerealistic andrefinedsafetyandriskhandlingprocedures.Finally,theframeworkinvitesforcombinedapproachestomodellingboth discreteandcontinuousaspectsinanintegratedwaywhileallowingthetime-scaleseparationthattypicallyexistsbetween hardwareandsoftwarecomponents.

Asanillustrativeexample,inourcasestudy,thesoftwareismodelledinRoboChart,whilethehardwareismodelledin Simulink. RoboChart [10] is adomain-specific language forthe model-basedengineeringofcontrol softwareforrobotics, thatcatersfortimedandfunctionalaspects.Itsformalsemanticsistailoredforreasoning,namelyusingtheCSP [54] model checkerFDR [13].However,itcurrentlylacksfacilitiestospecifythebehaviourofthehardware.Simulink [12],ontheother hand,isa defactostandard forcontrolengineering, typically usedfordynamic simulationinthe industrialsettingofthe HVC [5,6] system.

Formodelling, we useSimulink andRoboTool [11,9], that allowsthe graphical creationof RoboChartmodels, andfor verification we use Simulink Design Verifier (SDV) [12] and FDR. SystemProperty P1 is co-verified by model-checking, usingtheformalsemanticsofthecontrolsoftware,ascalculatedbyRoboTool,andanabstractspecificationofthehardware behaviour,asestablishedusingSDV.Theseareformalisedintock-CSP [54,55],thediscrete-timedprocessalgebraicsemantics ofRoboChart,forcheckingwithFDR.

Thecompletesystembehaviourisconsideredatasuitablelevelofabstractionforverificationby:(1)definingaplatform mapping; (2)usinga specificationofthehardware that captures atanabstract levelthe relationbetweenits inputsand outputs, asverifiedusingSDV;(3)formalisingtheseintock-CSP.Wedepict theapproachin Fig.8andexplain itindetail inthenext Section 4.1.In Section4.2we discussthe co-verificationofsystemproperties,modellingofthehardware and software,andthemechanisationinCSPoftheoverallframework. In Section5verificationofpropertiesofthesoftwareis alsodiscussed.

Fig. 8.Co-verificationframework,witharrowsindicatingthedirectionoftheinformationflowbetweeninputsandoutputs,ofthesoftwareandhardware models.Theplatformmappingcapturestherelationbetweenthesoftwareandhardwaremodeloneitherside.

4.1. Frameworkoverview

Inourframework, thesoftwareandhardware modelsare coupledviainterfacesthatcapturetheir inputsandoutputs, withconnectionsbetweenmodelsspecifiedviaplatformmappings.Ontheleft-handsideof Fig.8weconsidertheinterface of the HVCcontrol software,definedas a roboticplatform (RP1) in RoboChart, that specifies the inputsandoutputs as (possiblytyped)events,indicatedbysolidboxes.

Ontheright-handsidewehaveahigh-leveldescriptionofthehardwareplatform,thatcapturesitssensorsandactuators.

In ourabstraction ofthe HVCplatform,that comprises thecascadein Fig. 2,the hardware receives aninput voltage,via RPInputV_out,andproducesahigh-voltageviaRPActualHV_out.

We also annotate important assumptions aboutthe hardware that are of relevance for analysis: sensors are perfect, and,inparticular,thevoltageproducedviaRPActualHV_outisassumedtobethesameasthatsensedviaRPActualHV.The relationbetweenRPInputV_out andRPActualHV_outisestablished bythe Simulinkmodelasdetailedin Section4.2.2,but abstractedforverification,asexplainedlaterin Section4.2.4.TheinputsignalsRPerrorAckandRPsetPointareanabstraction overtheinputsavailabletoahumanoperator,whoseinteractionwiththesoftwareisrealisedviatheplatform.

Therelationbetweenthesoftwareandhardwaremodelisspecifiedbytheplatformmapping,asillustratedinthemiddle of Fig.8.Itrecordshowtheinputsandoutputsofthesoftwareareconnectedtosensorsandactuatorsofthehardwareplat- form,asrealisedbylow-levelcodeandphysicalinterfaces.Themappingsforthesoftwareinputsext_ActualHV,ext_errorAck andext_newSetPointaretrivial,asthesoftwarereadsdirectlyfromtheseidealisedsensors.Theinputext_pow24VStatus,of typePower,hasthevalueOnifthereadingfromthehardware,viaRPpow24V_inisbetween18and24Volts,andotherwise hasthevalueOff.

The softwareoutputsint_dutyCyclePWM1 andint_enablePWMareusedto determinewhethera voltageisproducedvia RPInputV_out.If the value set via int_enablePWM is true,then thevalue of RPInputV_out is determined by the value of int_dutyCyclePWM1, otherwise it is 0. This captures the fact that the PWM needs to be enabledin order to produce a voltage.Here,thefunctionduty2voltmapsapercentage,from0to100%totherangeoftheanalog0to10voltagesignalas previouslymentionedin Section3.

Moregenerally,whentheconnectionbetweensoftwareandhardwareisrealiseddirectlyviareadingandwritingtoreg- istersofsensorsandactuators,aplatformmappingcanbespecifiedbyarelation.AsinthecaseoftheinputRPpow24V_in, a voltageisrelatedtoadiscrete setofvaluesOnandOff.Ontheother hand,ifinputsofthesoftwareare interpretedas event-driveninterrupts,amoreappealingapproachistodefinewhenaneventisavailable [15] usingapredicateoverthe outputofoneormoresensors.Similarly,aninputtoanactuatormaybeconstrained,forexample,byapredicateoverone ormoresoftwareoutputs.

4.2. Systemverification

Usingtheco-verificationframeworkasillustratedin Fig.8,inthissectionweaddresstheformal verificationofsystem Property P1. As described in Section 3.1, it requires practical convergence of the high-voltage (RPActualHV_out) to the value of the setpoint as set by the user (RPsetPoint). Since the software is modelled in RoboChart, and the hardware in Simulink, our pragmaticverification strategy consistsof: (1) capturing P1 asa specification intock-CSP; (2) showing practical convergenceofthehardware outputRPActualHV_out inrelationtoits inputRPInputV_out usingSDV;(3)casting theresultobtainedfromSDVasatock-CSPspecification;(4)checkingwithFDRthat,whencombinedwiththesemantics

Table 1

tock-CSPoperatorsasusedinaTimedsection,withbasicprocessesatthetop,followedbycompositeprocesses:PandQaremetavariablesthatstandfor processes,a,c,anddforevents,gforacondition,andXforasetofevents.

Process Description

SKIP Terminating process

WAIT(d) Delay: terminates exactly afterdunits of time have elapsed STOP Deadlock: no events are offered, but time can pass USTOP Timelock: no events are offered and time cannot pass

a -> P Prefix operator: initially offers to engage in the eventawhile permitting any amount of time to pass, and then behaves asP if gthen PelseQ Conditional: behaves asPif the predicategis true, and otherwise asQ

P [] Q External choice ofPorQmade by the environment

P ; Q Sequence: behaves asPuntil it terminates successfully, and, then it behaves asQ P \ X Hiding: behaves likePbut with all communications in the setXhidden P |\ X Project: behaves likePbut with all communications not in the setXhidden P ||| Q Interleaving:PandQrun in parallel and do not interact with each other P [| X |] Q Generalised parallel:PandQmust synchronise on events that belong to the setX P[[ c <- d]] Renaming: replaces uses of channelcwith channeldinP

P /\ Q Interrupt: behaves asPuntil an event offered byQoccurs, and then behaves asQ P [| X |> Q Exception: behaves asPuntilPperforms an event inX, and, then behaves asQ TRUN(X) Continuously offers the events in the setXto the environment, while time can pass

timed_priority(P) Maximal progress: behaves asPwith internal behaviour given priority overtock, so that internal behaviour takes no time

oftheRoboChartmodel,viaamechanisationoftheframeworkdepictedin Fig.8,P1 issatisfied.ThatoverallpropertyP1 holdsisjustifiedbythetimedprocessalgebraicsemanticsofRoboChartandtheabstractspecification(2-3)asestablished usingSDV, andcapturedinCSP.Afull accountofthe CSPspecificationsforall ofthepropertiesconsidered inthispaper canbefoundonline.¹

Formalsemantics.Theformalismthat weuse,tock-CSP,isadialectoftheprocessalgebraCSP,wheretheeventtockmarks the passage of discrete time. As CSP adopts a reactive paradigm, interactions with the environment are specified using events, and that includes the passage of time in the case of tock-CSP. Importantly, it allows the specification of timed budgetsanddeadlines,andhasadenotationalsemanticsforrefinement [55].Relevantforourwork,themodelcheckerFDR hastailoredsupportfortock-CSP.

In Table1wesummarisethetock-CSPoperatorsthatweuseinourwork.Toillustratethenotationwepresentasimple CSPspecificationofaone-placetimedbufferin Listing1writteninCSPM,themachine-readableversionofCSPacceptedby FDR.Thedeclarationon line1introducesanamedtypedatawhosevaluesaredefinedbythesetofintegersbetween0and 2.Line2declarestwo typedchannelsnamed inandout,that canbeusedaseventconstructorsusingthedotnotation, forexample,in.0andout.1.Related,thesetofeventsgeneratedbyoneormoreeventconstructorscanbespecifiedasan enumeratedset,sothat,forexample,{|in|}isequalto{|in.0,in.1,in.2|},thesetofallinevents.

ProcessesdefinedwithinaTimedsection²(lines6-9)areinterpretedtobetimed:tockeventsareautomaticallyaddedto allowtimetopasswhenwaitingforinteractionswiththeenvironment,andthepassageoftimeisuniformacrossinteracting processes.The functionOneStep,definedonline4tobe 0forevery eventinits domain(indicatedby theunderscorein itssignature),ispassedasaparameter(line6)totheTimedsectiontoensurethatnotime isaddedimplicitlyafterevery synchronisationwiththeenvironment.

The behaviour of the timed buffer is that defined by the process Example (line 7) that behaves as TimedBuffer withtimed_priority applied,a function overprocesses, providedby FDR tocalculate thecorrecttimed semantics [55].

TimedBuffer(line8)initiallyofferstoreceiveadatavaluevia aprefixingonthechannelin,andthenoffersanexternal choice([]) totheenvironment betweenacceptinganewvalue,viatherecursiononTimedBuffer,ordelayingtheoutput ofthecurrentvalue,viaprefixingonoutafterthesequentialcomposition(;)withadelayofonetimeunit(WAIT(1)).We observethatanexternalchoiceisnotresolvedbythepassageoftime,butratherbysynchronisationonevents.Here,in?x issyntacticsugarforacceptingeventsin.xwherexrangesoverthetypedata.Theprefixingonout!xtakesthevalueof xasintroducedintocontextbytheprefixingonin?x.

Specification. Following the description of P1 in Section 3.1, here we construct a discrete version in tock-CSP, as shown in the RoboCharttimed csp block named SpecP1 in Listing 2. Itdeclares two channels (line 2), e andRPsetPoint, of type core_real.The eventeisused tomodel theabsolutedifferencebetween ActualHV_outandRPsetPoint,so that the specificationcancapturetherelationbetweenchangesinRPsetPointandtheabsolutedifference.

The behaviour of SpecP1SpecP1 is that of Follow, a process witha single parameterd, definedon lines 6-12 asan external choice ([]) over acceptingeventse orRPsetPoint,via prefixing(?x ->). Synchronisationon RPsetPoint,with anyvalue,ore,withvalue0,isfollowedbyarecursiononFollow.Whenevertheeventecarriesavaluethatisnot0(lines 8-9),thenFollowbehavesastheprocessADeadline({|e|},{|e.0|},d),thatensuresaneventewithavalueof0canonly beobservedwithindtimeunits(instantiatedas3s forSpecP1),andafterwardsbehavesasTRUN({|e.0|}).Thisbehaviour

1 https://github.com/UoY-RoboStar/hvc-case-study.

2 https://cocotec.io/fdr/manual/cspm/definitions.html#csp-timed-section.

1 nametype data = {0..2}

2 channel in, out : data 3

4 OneStep(_) = 0 5

6 Timed(OneStep) {

7 Example = timed_priority(TimedBuffer)

8 TimedBuffer = in?x -> (TimedBuffer [] (WAIT(1) ; out!x -> TimedBuffer)) 9 }

Listing1:Exampleofaone-placebufferthatisalwayspreparedtoreceiveavalue,butwhichdelaysitsoutputbyonetime unit.

1 timed cspSpecP1csp-begin 2 channele, RPsetPoint : core_real 3

4 Timed(OneStep) {

5 SpecP1 = timed_priority(Follow(s(3))) 6 Follow(d) = e?x -> (if x == 0

7 thenFollow(d)

8 else((ADeadline({|e|},{|e.0|},d) ; TRUN({|e.0|}))

9 /\ RPsetPoint?x -> Follow(d))

10 )

11 []

12 RPsetPoint?x -> Follow(d) 13

14 -- Allows time to advance by ’d’ units while events from ’S’ are performed 15 -- until an event from ’S’ that is in ’E’ is performed.

16 ADeadline(S,E,d) = EndBy(TRUN(S),d) [|E|>SKIP 17

18 -- Built into RoboTool: deadline for ’P’ to terminate within ’d’ units.

19 EndBy(P,d) = P /\ (WAIT(d);USTOP) 20 }

21 csp-end

Listing 2: Specification for PropertyP1defined within a RoboChart assertions’ process block namedSpecP1.

canbeinterrupted(/\online9)atanytimebyanewRPsetPoint.Weobservethatforthepurposeofmodel-checkingthe reals,modelledby thetypecore_real,are instantiatedinthediscretedomain0to2,sohereweconsiderthedifference e(t),encodedviatheevente,tobe0,withoutlossofgenerality.

TheauxiliaryprocessADeadline(S,E,d),definedonline16,takesthreeparameters,twosetsofevents,SandE,where S isexpectedto be a subset ofE,anda naturalnumber d. It continuously offersevents inthe setS, buttime can only advancebyuptodunits,unlessaneventfromthesetEhappens,inwhichcasetheprocessterminates.Itisdefinedusing theexceptionoperatorofCSP([|E|>),whereinitiallythebehaviouristhatofEndBy(TRUN(S),d),thatcontinuouslyoffers eventsinsetS,andallowstimetoadvancebyuptodtimeunits.Thus,withintheexception,ifTRUN(S)performsanevent thatisinE,thentheprocessbehavesasSKIP,thatterminatesimmediately.

We observethat theauxiliary processesTRUN andEndByare includedwiththeRoboTool distributionforconvenience.

EndBy(P,d), reproduced on line19, is a deadline over process P toterminate within dtime units.It behaves asP, but becausetimeisuniformintock-CSPitrequirestheright-handsideprocessWAIT(d);USTOPtoagreeonthepassageoftime.

Thatprocess,however,isonlypreparedtoletdtimeunitstopassbeforeittimelocks,effectivelyimposingadeadline.Next, wefocusonthehardwaremodel.

4.2.1. HardwaremodellingandverificationinSimulinkDesignVerifier(SDV)

Both the co-verification regime detailed in Section 4.1, as well as verification ofthe system-level properties, require a distinct and systematicseparation betweenhardware andsoftware components ofthe HVC system. Fig. 8provides an overview of thisseparation and the steps toward implementing thishave been set forward in the ingress of Section 4.

To thisend, the focusof thissection iscentred around hardware modelling, specification, abstraction andverification of hardwarepropertiesinSDV.Allofthesecomponentsarenaturallycombinedinordertoco-verifysystem-levelproperties.

Simulink is widely adopted asa tool fortraditional, input-driven simulation,and the modelling in SDV is similar to regular modelling used for simulation [12]. SDV uses Prover Plug-In^® products from Prover^® Technology to do model- checkingandprove themodelproperties [56]. Itisbuilt uponGunnar Stålmarck’sproofprocedure, whichusestautology checkstoprovethatanassertionholdstrueineverypossibleinterpretation [57].InPropertyProvingmode,SDVoffersthree differentproof strategies, Prove,FindViolation andProveWithViolationDetection wherethelatter ismerely a serial combination ofthe two first mentioned.In this work,both Proveand FindViolation havebeen used. Proveperforms an unboundedpropertyproof,whileFindViolationsearchesforpropertyviolationswithinthenumberofsteps specified by theMaximum violation steps option,which specifiesthemaximumnumberofsteps that SDVsearchesforproperty violations. Thus, verification with increasingly large Maximum violation steps will help to increase confidence in the property.

TheSimulinkmodel. The hardware modelinSimulinkwas createdbasedon previousmodels foundin [5,6].Thesemodels havebeen validatedboththeoretically andempirically byseverallabexperiments,andcorrespond well tothereal-world system. Inorderto doformal verificationwithSDV however,themodelhadtobe convertedfromcontinuous todiscrete

Fig. 9.Overviewofthehardwareverificationmodel.Thegreyboxincludesthemodellingofthecascade,whilethegreenboxcontainsthepropertyfor verification.

Fig. 10.Simulink model of the total CW-cascade hardware complementing the ideal model with loss and ripple terms [6].

time, since SDV doesnot supportcontinuous time. In this process,in addition to convertingtransfer functionsspecified in continuous time usingLaplace transform (S-domain) to discrete time Z-domain, some ofthe Simulink blocks specific tocontinuous timewere replacedwiththeirdiscretecounterparts. Fig.9showstheoverviewofthehardwareverification modelinSDVwheretheinput/outputsignals,i.e.,RPInputV_out andRPActualHV_outdenotethesamesignalsaspreviously introducedin Section4.1and Fig.8.Themappingandtransferfunctionbetweenthesetwosignals,andformalverification ofcertainhardware propertiestreatedinthissection,thencorrespondnaturally totheextension andscopeofthedashed greyboxontheupperrightsideof Fig.8.

Itisnoteworthythat,theinput,RPInputV_out,rangesoverthediscretedomain,{⁰,1,2}^{,andismultipliedbyaconstant} factor5inSimulink,effectivelycorrespondingtohavingthesetofpossiblevaluesof{⁰,5,10}^{voltbeingfedintothePWM} hardware model.Thismeansthat duty2volt mapsa percentage, from0to 100%totheentirerangeoftheanalogue [⁰¹⁰] voltage signal aspreviously mentioned in Section3.It also impliesthat theconvergence resultsobtainedin thissection using{⁰,5,10}^{voltasinput,willalsobevalidfortherealPWMhardwaresystem.Thisisbecauseitsinputset,}[⁰¹⁰]^,isa supersetof{⁰,5,10}^.

The test dataused tocreatethe modelwas collected fromstructured experimentsrunning atmanydifferentHV set- points,frequencies,distancesandnumberofstagesintheCW-cascade,providingarichdata-settorepresenthowtheactual hardwarewillbehaveintherealenvironment.Asdetailedin [5,6] anddepictedin Fig.10,theSimulinkmodelwill,inaddi- tiontotheidealtransferfunction,havetwoadditionaltermsdescribingthecascadelossandrippleeffects.UsingtheMatlab SystemIdentificationToolbox,state-spacemodelsandtransfer-functionsare fittedto thelabtest datatoprovidethebest descriptionofthePWMhardwaredynamics;bothduringthechargeanddischargemodesofoperation.Theresultingtrans- ferfunctionsandmodelcomponentsincontinuous timecanbe seenin Fig.10.Additionally,aSimulinkmodeldescribing thebell-cupinsidetheapplicatorthatwilleffecttheelectricalfield ataplaneatagivendistance,d,fromthepaintrobot, hasbeenderivedin [5] andusedhere.

In order to be able to formally verify the system-level property, P1, the mapping andrelational properties between RPInputV_out andRPActualHV_out,effectivelydescribing thehardware, isneeded. Thisallows ustoobtain awell-defined

“closedcircuit”mappingbetweenallofthecomponentsintheco-verificationframeworkof Fig.8.Tothisend,theSystem Identification Toolbox was used to model the transfer function describing the relation between these two signals (see Fig.11).Thisresultedinastandard,secondordertransferfunctionmodel:

G

(

s

) =

^Kp

(

1

+

^Tp1s

)(

1

+

^Tp2s

) ,

(3)

havingthefollowingspecificparameters K_p

=

¹

.

1196

Tp1

=

⁰

.

087821 T_p2

=

⁰

.

02042

.

Fig. 11.Simulinkmodeloftheidealcascadeincludingthemodemodelselectorandthetwotransferfunctionsdescribingthecharginganddischarging modesrespectively [6].

Fig. 12.SDV implementation of the PWM hardware convergence property,PHWas detailed in Eq. (4).

ThismodelwasthenanalysedinSimulinkwithparticularattentiontotimedynamics,stabilityandconvergenceproperties asdefinedby,e.g.,riseandsettling-time.Ofparticularinterestinthefollowing,isthesettlingtime,t_s,whichwasfoundto bets=⁰.3668 s.

Formalverificationofhardwareproperties. Based on the developed Simulink model, next, we will be verifying a low-level propertythatwillthenbeusedintheco-verificationschemeinordertoverifyPropertyP1.

Referring back to the definition of PropertyP1, the error term Eq. (1) as well as the notion of practicalconvergence in Section3.1,thefollowinghardwarepropertywillbeconsideredandverifiedinthissection:

P_HW: Practical convergence of actual hardware output voltage, RPActualHV_out, to the hardware input signal, RPIn- putV_out,withinsettlingtime,ts:

∀

^t

≥

^tsp

+

^ts

=⇒

E

(

t

) = |

RPInputV_out

(

t

) −

RPActualHV_out

(

t

)| −

0

.

15

×

max

(

RPInputV_out

(

t

),

1

) ≤

0

.

(4) Here, t_sp denotes the time instance wherean update to the input, RPInputV_out, isreceived inPWM hardware. It is notablethatwhilePropertyP1isasystem-levelproperty,involvingbothsoftwareandhardwarecomponents,PropertyPHW as definedby Eq. (4) serves asa low-level hardware property. Anotherimportant distinction, stems fromthe difference invalue betweenthesettling time,ts=⁰.3668 s, in Eq. (4) and

τ

₌3 s in Eq. (1) whichimpliesthatPHW incrementally contributes towards fulfilment of corresponding equations to verify the overall convergence Property P1. This fact also underliesandexplainsthedifferenceinpeakdeviationlimit(0.15and0.3respectively)betweenthetwoproperties.

TheSimulinkimplementationtoverifythispropertylieswithinthegreenVerificationSubsystemin Fig.9andhasbeen depictedin Fig. 12. Theupperpartcontaining theDetectChangeblock andan integratorfunction,worksasa timerthat is resetevery time thereis a changein RPInputV_out.This inorder to capturethet≥^tsp+^ts constraintin Eq. (4).The lower part takesthe absolutevalue of the error betweenRPInputV_out andRPActualHV_out andsubtracts the accepted error,which issetto0.15×^max(RPInputV_out(t),1).Finally,the lastfunction ontheright, denotedevaluation, givesout false if Eq. (4) is notfulfilledatanytimeinstance,t≥^tsp+^ts.Otherwiseitgivesout true.Thisisverifiedwiththeproof assumptionblock,whichshowsifthepropertyisfulfilledorviolated.

Table 2

Resultsoftheverificationofthehardware,usingFindViolationanddifferentvaluesforMaximumviolation steps. Maximum

violationsteps

Fixed-stepsize

(fundamental sample time)

Result Elapsed time

1,000 1e⁻⁶ Valid within bound 0:47:49

1,000,000 1e⁻⁶ Valid within bound 0:46:44

1,000,000,000 1e⁻⁶ Valid within bound 0:47:15

2,147,483,647 1e⁻⁶ Valid within bound 0:47:15

Fig. 13.RoboChartmodelcomponents:roboticplatform( RP1),interfaces(namedIOps,IEvents_RP1,IEvents_ext,andSharedVars_all),enumerated(Power andState)andgiven(duty)datatypes. isanevent, isavariable,and isassociatedwithanoperation. isusedtorecordthataninterfaceis provided,while isausedinterface.

After creatingthemodelandthespecification, theProvestrategywasusedinordertoverifytheproperty. Itwasrun both usingMATLAB onlineandona Windows laptop withIntel^® Core^© i5CPU@ 2.71 GHz. The onlineversion and the desktopversionwerebothusedinordertoruntwoverificationsinparallel,toseeifonewouldproducearesultfasterthan theother.However,afterrunningbothcontinuouslyfor10dayswithoutproducingaresult,theverificationwas manually terminated, withthe assumptionthat the complexity hadresultedina state-space explosionthat madeSimulink unable toverifythespecification.Itwasinsteaddecidedtogain increasedconfidenceintheverificationbyusingFindViolation withincreasingMaximum violation steps.TheresultsoftheverificationbyusingFindViolationcanbeseenin Table2.

TheMaximum violation stepsoptionwasgraduallyincreased,untilreachingthemaximumvalueof2,147,483,647,which isthemaximumvaluefordatatypeint32.Asseeninthetable,SDVwasabletoprovethatthepropertywasvalidwithin boundinallcases.

4.2.2. SoftwaremodellinginRoboChart

Inthissection,wepresenttheRoboChartmodelofthesoftware,thatisaformalisationofthesketch previouslyshown in Fig. 7.Theroboticplatform(RP1)–aspecificationoftheservicesavailabletothesoftwareintermsofvariables,events and operations– isfully specified in Fig.13. Its events are definedin theinterface IEvents_RP1. RP1 also provides the interfaceSharedVars_all,thatdeclaresallofthesharedvariablesthatareusedinthemodel.TheinterfaceIOpsspecifiesthe signature ofthesoftwareoperationsthatareused,anddefined, intheRoboChartmodel.Inadditiontoemployingbuilt-in datatypes,suchasreals,naturals,andbooleans,threedatatypesaredeclared:theenumeratedtypesPowerandState,and thegiventype duty.Twofunctionsmsandsareusedto constructtimeunitscorresponding tomillisecondsandseconds, respectively.RoboChartadoptsthetypesystemofZ [58,59].Forafullaccountofthelanguageanditsformalsemanticswe referthereaderto [11,16,9].Here,wedescribetheRoboChartconstructsasweusethemtomodelourexample.

Moduleandcontrollers.Thetop-levelcomponentofthesoftwaremodelisdefinedbytheRoboChartmodulemod_sys,shown in Fig.14.Itassociatestheroboticplatformwithfourcontrollers (ctrl0-3), thatcapturespecificbehaviours. Controllerctrl0, shownin Fig.15,contains themainState_machine,thatisarecastofthatpresentedin Fig.7,ctrl1capturesthebehaviour ofthewatchdogs,andcontrollers ctrl2-3are usedtorelayevents.Controllerctrl2relaystheinput eventext_pow24VStatus fromRP1tocontrollersctrl0-1,andctrl3relaystheoutputeventsint_dutyCyclePWM1andint_enablePWMfromctrl0andctrl1 toRP1,asRoboCharteventconnections arepoint-to-point.Duetotheirsimplenature,thefull definitionofallcontrollers is deferredtoan on-linereport.³ In RoboChart,connections withtheplatform arealways asynchronous,indicated by the

3 https://robostar.cs.york.ac.uk/case_studies/hvc/.

Fig. 14.RoboChartmodulemod_sysdefiningtheconnectionsbetweencontrollersandtheroboticplatform.Controllerctrl0containsthemainState_machine, arecastinRoboChartofthestatemachinepresentedin Fig.7.Thewatchdogshavebeencombinedintoonestatemachine,definedinsidecontrollerctrl1.

Controllerctrl2relaystheeventext_pow24VStatustocontrollersctrl0andctrl1,whilecontrollerctrl3isusedforrelayingtheeventsint_enablePWMand int_dutyCyclePWM1toRP1.

Fig. 15.Controllerctrl0, showing its inputs and output connections toState_machine, and references of operations.

keywordasync,asinteractionswiththeplatformcannot berefused,onlyignored [10,p. 3110].Theconnections between allcontrollersctrl0-3,however,aresetassynchronous.

Statemachine. The corebehaviour ofthe HVC controller iscaptured by theState_machine in Fig. 16.In RoboChart, state machinesare self-containedby explicitly statingtherequired ( ) variables andoperations, andtheused ( ) events.In thiscase,State_machinerequiresthesoftwareoperationsdeclaredinIOps,andthesharedvariablesinIVars_seqSM_shared.

Italsodeclares:localvariablesviatheinterfaceIVars_seqSM,aconstantcycleTimewithadefaultvalue of10milliseconds, andaclock( )Cl1.ItusestheeventsofinterfaceIEvents_ctrl0,thatarealsoexplicitlylistedontheleft-handsideof Fig.16.

Fig. 16.MainState_machinecorresponding to that of Fig.7recast in RoboChart.

The executionflow ofState_machine starts attheinitial junction,followed by a transitionwhoseaction, specifiedaf- ter the dash (/), initialises the value of the variables mSetPoint and HVEnabled, by assigning 0 and false in sequence (;), respectively. It then waits for cycleTime units before entering state Init. This initial delay is a simplification of the GateDriverRamping behaviour depicted in Fig. 7, which does not concern the properties of interest for verification. In stateInitthereisan entryactionthatcallsthesoftwareoperationAdjustLimitswhichcalculatesthevalueofvariablesover- LimitandunderLimitandisdefinedbyastatemachineasshownin Fig.17.TherequiredvariablesofAdjustLimits,aslistedin interface IVars_adjustLimits,areprovided byState_machineinthecontextofthecalltoAdjustLimits,effectivelysharingthe state.

After the initialisation iscomplete,the executionproceedstothe compositestate Wait24Vpower onthenext cycle. Its entryactionexplicitlyrecordsthatthestatehasbeenenteredbysettingthevariablecurrentState.ThetransitiontoClosed- LoopisonlyenabledwhenthecurrentvalueofsetPointis0,the24 V powerisstable(pow24VStatus==Power::On),andthe ErrorMode isnot activated,asindicatedby thetransition’sguard.Thebody ofWait24Vpowermonitors therelevantinputs periodicallyaspartofthecycleoftransitionsbetweenthejunctions.Firstly,theoperationsdisableHVandsupplyVoltCheck, asdefinedin Fig.17,arecalled. disableHVdisablesthehigh-voltage,whilesupplyVoltCheckcheckstheinput ext_pow24VS- tatusandupdatesthevalueofthevariablepow24VStatus.Secondly,thevalueofthevariablesetPointisalsoupdatedviaa reading(ext_setPoint?setPoint)through eventext_setPoint,withadeadline (<{0}) ofzerotime units.InRoboChartbudgets anddeadlinesmustbespecifiedexplicitly,andsoherethedeadlineindicatesthatthereadingtakesanegligibleamountof time.

Fig. 17.SoftwareoperationsmodelledinRoboChartwiththeirbehaviourdefinedbystatemachines:disableHVdisablesthehigh-voltagebywritingfalseto int_enablePWMandsettingthedutycycletozeroviaint_dutyCyclePWM1;enableHVenablesthehigh-voltage;AdjustLimitscalculatesvoltagelimits,overLimit andunderLimit,basedonthecurrentvalueofmSetPoint;andsupplyVoltCheckcheckswhetherthe24 V powerisstableviatheinputext_pow24VStatus,and ifunstablecallsdisableHV.

Fig. 18.Watchdogstatemachine.Initiallythereisadelayof4millisecondsbeforeengaginginacyclicbehaviour.FirstAdjustLimitsiscalled,andafter2 millisecondssupplyVoltCheckiscalled,withsamebehaviourrepeatedafteradelayofafurther8milliseconds.ThecalltosupplyVoltCheckcandisablethe high-voltageifthe24 V powerisnotstable,asshownin Fig.17.

The criticalphase ofHVC operationis capturedinstate ClosedLoop,that controlsthePWM. Initially theuser-defined setpoint,ext_SetPoint,isreadintothevariablesetPoint.Ifthevalueiszero,thendisableHViscalledtoensurethatthehigh- voltageisdisabled.Afterwards,ifthevalueisnon-zeroandthehigh-voltagehasnotbeenenabledyet(HVEnabled==false), HVEnabledissettotrue,thesupplyvoltageischeckedbycallingsupplyVoltCheck(),andthehigh-voltageisenabledbycalling enableHV. While thehigh-voltage isenabled, theinternal setpoint (recorded invariable mSetPoint) is adjustedby calling setPointRamping(setPoint).ThePWMduty-cycleisadjustedbyPID_Controlthatoutputsapercentageviaint_dutyCyclePWM1, according to the difference between mSetPoint and ActualHV, the measured high-voltage via the input ext_ActualHV. In state s0ofClosedLoop,theflowofexecutionmaybeinterruptedbytransitioningtoErrorModewhencurrentStateissetto State::ErrorMode.Theerrorcanbeacknowledgedviatheeventext_errorAckwithinthecurrentcycleTime,afterwhichthere isatransitiontoWait24Vpower.

ThevariablecurrentStatemaybesettoState::ErrorModebycallingdisableHV(true),eitherwhileinWait24Vpower,orfrom within operationscheckLimitsorsupplyVoltCheck,thatcheckswhetherthe input24 V power isstable.The latteriscalled regularly instatesClosedLoopandWait24VpowerofState_machine,andalsobythewatchdog,which,aswillbe explained next,ismodelledinanotherstatemachine.

Watchdog.Thewatchdog,shownin Fig.18,executes,over time,inalternationwiththemainState_machine,thatexecutes on a10millisecondcycle, asspecifiedby theconstant cycleTime.Therefore,thewatchdog’sbehaviour isinitially delayed by 4 milliseconds.In state s0 thereis a callto AdjustLimits(), and2 milliseconds later, theoperation supplyVoltCheck() is called.Weobservethatthetransitionbetweens1ands0takes8milliseconds,anditisduringthistimethatState_machine actuallyexecutesitscyclicbehaviour.