DOC

Service Ballistic Computer Programming Based on B-Method

By Gladys Powell,2014-02-17 20:09
10 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

    CONSTANTSDlEDOUBLEAEDOUBLEAA1EDOUBLE

    AA2?DOUBLE

    INVARIANTdisED1..D2AEA1.A2AtEDOUBLEA INITIALIZA

    T10N

    unrEN3OLAfEDOUBLE×DOUBLE×DOUBLE

    --

~DOUBLE×DOUBLEA(MrV(dgv,t)=

    ,(0,dis,))

    dis:?D1..D2lla:EA1..A2t:=0IIurlr:=

    TRUEllf:EDOUBLE×DOUBLE×DOUBLE--"

    DOUBLE×DOUBLE

    OPERAT10NSCALCULATE

    BEGIN(dgv,f):=,(vo,dis,)

    uT/r:=BOOL(妇口:EDG.DG2)

    IFu71r=TRUETHENdgv:EDGI..DG2END

    END

    disrepresentsthedistancebetweentheshooting pointandthetarget,i.e.,thelengthofthelineof sight;representstheverticalanglebetweentheline ofsightandthehorizontalline;trepresentsthetime spanfromshootingtohitting:rrepresentsa

    Booleanvariablethatindicateswhetherthetargetis outofthefiringrange.

    BASICSTATBALalsodefinesaballistic

    curvefunctionftocalculatedgvandt.Thelast conjunctivec[auseofitsINVARIANT,whichimplies thateitherthetargetisunreachable(firingforbid

    den)ortheresultoffiringistohitthetarget,isa keytothesoftwaresecurity.

    Fig.2Relevantparametersforshootingattarget Takingthehorizontalanglebetweentheplaneof fireandthelineofsightintoconsideration(thatis, theprojectilelineandthelineofsightdonotfallinto thesameverticalplane),theplaneoffireneedstobe horizontallyrotatedwithanangleJ9beforefiring,

MACHINESTATBALinTable3carriesoutthis

    f1ruction.

    

    180

    Table3AMSTATBAL

    MACHINEBASICSTATBAL INCLUDES

    PR0MOTES

    VARIABLES

    C0NSTANTS

    INVARIANT

    INITIALIZATION

    0PERAT10NS

    BASICSrArBAL

    CALCULATE

    |8

    B1EDOUBLEAthEDOUBLE .8EB1..B2

    :=0

    ROTATEBEGINskipEND AMsinTable4and5

    shootingatmovingtargets carryoutthefunctionof Similarly,BASICDY

    NABALconsiderstheconditionthatthelineof

    sightandthemovingdirectionofthetarget(withve locity"andverticalangle),,aspartlyillustratedin

    Fig.2)fallintothesameverticalplane,whereas

    DYNABALdealswiththetargetwithamovingve

locityconsistingofthecomponentintheplaneof

    fireandthecomponentverticaltou. Abovemachinescanfurtherberefinedorex

    tendedintomorecomplicatedmachines,e.g.,guided andautomaticseparatingballisticcomputers. 2.2ImplementationofBallisticFunctions ExceptSIMPLESTBAL,eachcarrierindepen

    dentAMneedstohaveitsownIMPIEMENTA

    TIONthatcanbedirectlytranslatedintoanexe

    cutableprogram;eachIMPLEMENTATIONfurther importsamachinetoperformthecalculationofre

    ZHENGYu-jun,eta1./GeneralServiceBallisticComputerProgrammingB.s0BM?^0

    quiredballisticfunctions.Forexample,Fig.3shows theimplementationarchitectureofBASIC——STAT——

    BAL,whoseballisticfunctionfiscalculatedbyma

    chineSTATBALCAL,whichincludesaseriesof machinestocalculatetheeffectofvariousdisturbance

    factorsincludingaerodynamicalresistance,airchurn

    ingresistance,windage,hydraulicresistance,atmo

    sphericdisturbance,deformationresistance,etc. Table4AMBASICDYNABAL

    MACHINESI?IEBAL

    REFINESBASICSBBAL

    ?RIABU",),

    IN?RI"?0A),?0..2

    INITAIIZA.

    ":=0f),:?0..2n

    T10N

Report this document

For any questions or suggestions please email
cust-service@docsford.com