搜索
UsingHYTECHtoSynthesizeControlParametersforaSteamBoiler*ThomasA.ttenzinger1HowardWong-Toi21DepartmentofElectricalEngineeringandComputerSciencesUniversityofCalifornia,Berkeley,CACadenceBerkeleyLabs,Berkeley,CAAbstract.Wemodelasteam-boilercontrolsystemusinghybridau-tomata.Weprovidetwoabstractedfinearmodelsofthenonlinearbe-havioroftheboiler.Foreachmodel,wedefineandverifyacontrollerthatmaintainssafeoperationoftheboiler.Thelessabstractmodelpermitsthedesignofamoreefficientcontroller.WealsodemonstratehowthetoolHYTECHcanbeusedtoautomaticallysynthesizecontrolparameterconstraintsthatguaranteesafetyoftheboiler.1IntroductionAdescriptionofanindustrialsteamboilerhasbeenproposedasabenchmarkproblemfortheformalspecificationandverificationofembeddedreactivesys-tems[1,2].Ourapproachtotheproblemisuniqueinthatweusealgorith-mictechniquestoanalyzedirectly,withoutdiscretization,themixeddiscrete-continuouscomponentsofthesystem.Inthiswayweareabletofullyauto-maticallysynthesizesafevaluesfortheparametersthatcontrolthecontinuousbehavioroftheboiler.Wedescribethesteamboileranditscontrollerusinghybridautomata[4,3].Theseautomatamodelnondeterministiccontinuousactivitieswithinanondeter-ministicdiscretetransitionstructure.Sincethenonlinearbehaviorofthesteam-boilersystemisnotdirectlyamenabletoautomaticanalysis,weprovideanapproximatingmodelusinglinearhybridautomata.Linearhybridautomataareasubclassofhybridautomatawithlinearityrestrictionsoncontinuousactivities(inequalitiesbetweenlinearcombinationsoffirstderivatives)anddiscretetransi-tions(inequalitiesbetweenlinearcombinationsoftransitionsourcesandtargets).Model-checkingbasedanalysistechniques[5]forthissubclasshavebeenimple-mentedinHYTEctt[16,17]andusedtoverifynumerousdistributedreal-timesystems[14,19].Borrowingideasfromthefieldofabstractinterpretation[9,15],wechooseourapproximationssuchthatifadesiredpropertyholdsforanap-proximatinglinearautomaton,thenitholdsalsofortheoriginalnonlinearau-tomaton.*ThisresearchwassupportedinpartbytheONRYIPawardN00014-95-1-0520,bytheNSFCAREERawardCCR-9501708,bytheNSFgrantCCR-9504469,bytheAFOSRcontractF49620-93-1-0056,andbytheARPAgrantNAG2-892.266Wealsotakealgorithmicanalysisastepbeyondthecheckingofsystemprop-erties.Givenaparametricdescriptionofacontroller,weuseHYTECHtoau-tomaticallysynthesizeconstraintsonthesafevaluesforthecontrolparameters[6,10].Theseconstraintsarenecessaryandsufficientforthecorrectnessoftheapproximatinglinearautomaton,andbecauseofourchoiceofapproximations,theyarealsosufficient(thoughnotnecessary)forthecorrectnessoftheoriginalnonlinearautomaton.Moreaccurateapproximationsthusprovidelessrestric-tiveconstraintsonthecontroller,whichcanbeusedtocontrolthesystemmoreefficiently.Steam-boilerdescription.Thesteamboilerconsistsofawatertank,fourpumps,andsensorsthatmeasurethepumpingrates,thesteamevacuationrate,thewaterlevel,andtheoperationalstatusofeachcomponent(seeFigure1).Theentirephysicalsystemoperatesundertheguidanceofacontroller.ThecontrollermustkeepthewaterlevelbetweentheextremevaluesM1andM~atalltimes,anditshouldtrytokeepthewaterlevelbetweenthenormaloperatinglevelsofN1andN2asmuchaspossible.Allcommunicationbetweenthecontrollerandthephysicalplantoccursindiscreterounds,onceeveryAseconds.Ineachround,allunitssendinformationtothecontroller,andthecontrollerrespondsbysendingmessagestotheunits.Allcommunicationisassumedtotakeplaceinstantaneously.Thecontrolleroperatesinfivemodes:initialization(waitingforthesteamboilertosignalitsreadinessforoperation),normal,rescue(thewater-levelsensorhasfailed),degraded(othercomponentshavefailed,butthewater-levelsensorisworkingcorrectly),andemergencystop.Intheinitializationmode,thecontrollerreceivesasignalthattheboilerisready,andthenteststheamountofsteamescapingfromtheboiler.Ifthisisnonzero,itenterstheemergencystopmode.Otherwise,iteitherdrainsthewaterlevelto?/2oractivatesapumptoraisethewaterleveltoN1.Oncetherangeofnormalwaterlevelshasbeenreached,thecontrollersendsasignaltothephysicalunits,waitsforacknowledgements,andthenproceedswithnormaloperation.Innormalmode,thecontrollermakesitsdecisionstoturnpumpsonoroffbasedonthecurrentwaterlevel,thestatesofthephysicalunits,andtherateatwhichsteamisbeingemitted.Noactionistakenifthewaterlevelliesintherange[N1,N~].Indegradedmode,someunit,otherthanthewater-levelsensor,hasfailed.Messagesaresenttorepairthefaultycomponents,andthecontrollerattemptstomaintaincorrectwaterlevelswiththeoperationalcomponents.Thereaderisreferredto[2]foradescriptionoftherescuemode.Ourgoalisnottoprovideadetailedmodelofthemessagepassingbetweensystemcomponentsandthecontroller;todosowouldresultinstateexplosion.Rather,wefocusonthehigh-levelinteractionsbetweendiscretecontroldeci-sionsandthecontinuousaspectsoftheunderlyingphysicalplant.Tothisend,werestrictmostofourdiscussiontotwofault-freepumpsinnormaloperatingmode.Thissimplifiesthediscretecontrolspaceofthesystemandallowsustoconcentrateonthecontinuousevolutionofvariablesmodelingthewaterlevel,steamandpumpingvolumes.Onlyinalatersectiondowebrieflyconsiderfour267wM2--VI--UmN2--waterNiLLI