DOC

Service Ballistic Computer Programming Based on B-Method

By Gladys Powell,2014-02-17 20:09
13 views 0
Service Ballistic Computer Programming Based on B-Method

    Service Ballistic Computer Programming

    Based on B-Method

    JOURNALOFCHINAORDNANCE

    ArticleID:1673002X(2006)03.0178O6

    General-ServiceBallisticComputerProgramming

    BasedonB.Method

    ZHENGYujun(郑宇军),ZHANGZiqiu(张子丘),WANGJinquan(王金全).,

    XUEJinyun(薛锦云)'4

    1.InstituteofSoftware,ChineseAcademyofSciences,Beijing100080,China; 2.ArmamentDemonstrationandResearchCenter,Beijing100034,China; 3.SystemEngineeringResearchInstituteofEngineerEquipment,Beijing100093,China; 4.CollegeofComputerInformationEngineering,JiangxiNormalUniversity,Nanchang330027Jiangxi,China

    Abstract:Formalmethodsofferthepromiseofsignificantimprovementonqualityandreliabilityofcriticalembeddedsoft.

    ware.BMethodisemployedtodevelopgeneral

    serviceballisticcomputerprogramsinthepaper,eachofwhichcanbe

    adaptedtoafamilyofservice/weapon

    specificballisticcomputers.BasedonthestructuringmechanismsofB.method,a unifiedapproachisproposedtosystematicallycontrolthecomplexityofballisticparametersintheprocessoftypeandoper.

    ationrefinement,andultimatelyaseriesofhighreliable,reusable,andscalableprogramsareproduced.Experienceswith

    theapplicationofthemethodandtoolsarealsodiscussed.

    KeyWords:B

    Method;ballisticcomputer;programming;abstractmachine(AM);refinement Introduction

Embeddedrealtimesoftwarehasbeenwidely

    usedtomonitorandcontrolthesafetycriticalsys

    tems.Iftheembeddedsoftwareinthesafetysystems failstoperformtheintendedfunctionsorfailstomeet thestringentconstraints,itmayposeseriousriskto personnelandtheenvironment,causingcatastrophic results.Overthepasthalfcentury,toimprovesys

    temsafety,reliabilityandavailabilitymainlydepend

    edonsoftwaretestingandfaulttolerance.Inrecent years,theformalmethodshavebeenincreasingly usedindesigning,specifying,andverifyingcritical softwaresystems,andofferthepromiseofsignificant improvementofqualityandreliability.TheB

    Method[.afirstofitskindcoveringsoftwarepro

    cessfromabstractspecificationstoexecutableprod

    ucts,hasbeensuccessfullyusedindifferentindus

    tries[23..

    However,untilnowfewresearcheshave

    reportedabouttheapplicationoftheBMethodin

    militarysoftwaresystemswheresecurityisof paramountimportance.

    Thepaperpresentsanapproachofballisticcom

    puterprogrammingusingBMethod.Thedevelop

    mentprocessstartswithanAMwhichspecifiesthe simplest,generalserviceballisticcomputer;existing AMsarethenenhancedtomorepowerfulgenera1..ser.. vicecomputersbygraduallyintroducingnewballistic functions;thosegeneralservicecomputersarefurther

    specializedtoconcretecomputersbyaddingservice/

weaponspecificproperties.

    OverviewofB.Method

    I,heBMethodisatheorybased.modeloriented

    formalmethodforspecifying,designingandcoding softwaresystems[,.

    Itsupportsmodularstruc

    turingbasedonacollectionofstructuringmechanisms forinformationhiding,modularizationandthecom

    positionalityofmoduleoperations,reuseandproof decompositionJ.

    Systemsaremodeledasacollection

    Received2005.1027

    SponsoredbyNationalNaturalScienceFoundation(60273092,60573(180)andNationalGr

    andFundamentalResearch973ProgramofChina (2003CCA02800)

    

    178

ZHENGYu-jun,eta1./General

    ServiceBallisticComputerProgrammingBasedonB-Method ofinterdependentAMs,forwhichanobjectbased

    approachisemployedatallstagesofdevelopment. TherearethreemaintypesofAMsinBMethod.

    1)MACHINE:representsan(initia1)AMthat encapsulatesastateconsistingofasetofvariables constrainedbyaninvariant,andoperationswhich maychangethestateandreturnasequenceofresults whilemaintainingtheinvariant.

    2)REFINEMENT:representsan(intermedi

ate1AMthatrefinesaMACHINEoranotherRE

    FINEMENTbyreplacingitsstatewithmoreconcrete stateand/orreplacingitsoperationswithmorecon

    creteoperations.

    3)IMPLEMENTATION:representsan(ulti

    mate)AMthatneedsnottobefurtherrefinedand canbeimplementedwithexecutableprogramlan

    guagesorhardware.

    Method,largeAMscanbeconstructed InB

    fromotherAMsusingthefollowingclauses. 1)INCLUDES:Itallowstheseparatedpartsof systemstatetobecombinedintoasingle"including" AM.

    2)USES:Itallowsa"using"AMtoreference al1thevariablesoftheusedmachine. 3)IMPORTS:ItallowsanIMPLEMENTA

    TIONtobeconstructedfromanumberoflowerlevel

    AMs.

    4)SEES:ItallowsaREFINEMENToranIM

    PIEMENTATIONAMtogainaccesstoshareddata ofa"seen"machine.

    TheBMethodissupportedbytheBToolkit[,

    whichprovidesautomaticfeaturesincludingsyntax andtypechecking,proofobligationgeneration,prop

    ertiesproving,failedproofexploration,symbolicani

    mation,andcodegeneration.Theextensivetoolsup

    portisamajorfactorinourchoiceoftheBMethod.

    2DevelopmentProcess

    Eachballisticcomputercanbemodeledasan AM,whichdescribesoperationsthatinterfacewith

    theprogramaswellastheoperationsrequiredtobe performedbytheprogram.Ourdevelopmentprocess startswiththesimplestballisticcomputer;bygradu

    allyintroducingnewfunctions,theexistingAMsare enhancedtomorecomplicatedAMswhichrepresent morepowerfulballisticcomputers.AsshowninFig. 1,AMsintheleftpartarecarrierindependentma

    chines,i.e.,ballisticcomputersthatperformfunc

    tionsindependentofservicesandweapons;incon

    trast,AMsintherightpart,orcarrierdependent

    machines,performfunctionsconcerningtheproper

    tiesofconcreteweaponswhichareequippedwithcar

    rier-dependentmachines,andtheinfluencesofmis

    sionswhichareassignedtothose.

    carrier-independentAMs!carrier-dependentAM SIMPLESTBALil

    ?

    lk.

    ?

    ~IAI

    -

    Dt

    :t

    L

    ?;

    ;

    !,

    .

    "

    ,

,

    ,

    ?.u.._--"6Xiii

    BASICCYNABAL:.,j.

    

    …一0i

    =

    REFINES

    ————一…..'

    INCLUDESEES

    Hg.1Developmentprocessofbailisticcomputerprograms 2.1BasicBallisticComputers

    Thereisjustonethingforthesimplestballistic computerSIMPIESTBALinTable1todo:shoot

    offanyway.Inotherwords,themachineselectsan arbitraryvalueinthedomainsofthemuzzlevelocity 0andthefireangledgv,respevtively.(Fordiffer

    entmetricsforthevelocityandtheangle,DOUBLE canbesubstitutedwithothertypessuchasFLOAT, INTEGER,etc.)

    Strictlyspeaking,thespecificationshouldfur

    thercontaintheoperationstochangethevalueof muzzlevelocityandfireangle.Butsuchoperations arequitestraightforwardandcanalwaysbeimple

    menteddirectlybyhardware,andthereforeareomit

    tedinthepaper.

    ObviouslynobodywilluseSIMPLEST——BAI.

    MachineBASICSTATBALinTable2achievesa morepracticalgoal:shootatastationarytarget.Be

-——

    179-——

    一一?一一?一一??

JOURNALOFCHINAORDNANCE,2006,go1.2,No.3

    sidesINCLUDEwithSIMPLESTBAL,itintro

    ducesthefollowingnewvariables(aspartlyshownin

    Fig.2).

    BAL Table1AMSIMPLEST

    MACHINESIMPIESTBAL

    ,RIABlSvo,dgv

    CONSTANTSVl?DOUBLEAv2?DOUBLEA

    DGIEDOUBLEADEDOUBLE

    INVARIANTvo?V1..V2AdFo?阱1..DG2

    INITIALIZATION0:EVI..lldFv:EDG1.. 0P1II()NSCALCULATE

    PREvoEVI..V2AdffvEDG1..DG2THENskip END

    Table2AMBASIC..STAT..BAL MA【?NEBASICSDEL

    REFINESSIMPLESt一队L

    vARlABIESdis,,t,u71r