Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Synchronous Functional Programming: The Lucid Synchrone Experiment

De
30 pages
Synchronous Functional Programming: The Lucid Synchrone Experiment ? Paul Caspi † VERIMAG Grenoble Gregoire Hamon The MathWorks Boston Marc Pouzet ‡ LRI, Univ. Paris-Sud 11 Orsay 1 Introduction Lucid Synchrone is a programming language dedicated to the design of reactive systems. It is based on the synchronous model of Lustre [25] which it extends with features usually found in functional languages such as higher-order or constructed data-types. The language is equipped with several static analysis, all expressed as special type-systems and used to ensure the absence of certain run-time errors on the final application. It provides, in particular, automatic type and clock inference and statically detects initialization issues or dead-locks. Finally, the language offers both data-flow and automata-based programming inside a unique framework. This chapter is a tutorial introduction to the language. Its aim is to show that techniques can be applied, at the language level, to ease the specification, implementation, and verification of reactive systems. 1.1 Programming Reactive Systems We are interested in programming languages dedicated to the design of reactive systems [31]. Such systems interact continuously with their external environment and have to meet strong temporal constraints: emergency braking systems, plane autopilots, electronic stopwatches, etc. In the mid-70's, with the shift from mechanical and electronic systems to logical systems, the question of the computer-based implementation of reactive systems arose.

  • based

  • languages while

  • start

  • synchronous languages

  • purpose programming

  • version scade

  • physical time

  • scade comes


Voir plus Voir moins
SynchronousFunctionalProgramming:TheLucidSynchroneExperimentPaulCaspiGre´goireHamonMarcPouzetVERIMAGTheMathWorksLRI,Univ.Paris-Sud11GrenobleBostonOrsay1IntroductionLucidSynchroneisaprogramminglanguagededicatedtothedesignofreactivesystems.ItisbasedonthesynchronousmodelofLustre[25]whichitextendswithfeaturesusuallyfoundinfunctionallanguagessuchashigher-orderorconstructeddata-types.Thelanguageisequippedwithseveralstaticanalysis,allexpressedasspecialtype-systemsandusedtoensuretheabsenceofcertainrun-timeerrorsonthefinalapplication.Itprovides,inparticular,automatictypeandclockinferenceandstaticallydetectsinitializationissuesordead-locks.Finally,thelanguageoffersbothdata-flowandautomata-basedprogramminginsideauniqueframework.Thischapterisatutorialintroductiontothelanguage.Itsaimistoshowthattechniquescanbeapplied,atthelanguagelevel,toeasethespecification,implementation,andverificationofreactivesystems.1.1ProgrammingReactiveSystemsWeareinterestedinprogramminglanguagesdedicatedtothedesignofreactivesystems[31].Suchsystemsinteractcontinuouslywiththeirexternalenvironmentandhavetomeetstrongtemporalconstraints:emergencybrakingsystems,planeautopilots,electronicstopwatches,etc.Inthemid-70’s,withtheshiftfrommechanicalandelectronicsystemstologicalsystems,thequestionofthecomputer-basedimplementationofreactivesystemsarose.Atfirst,theseimplementationsusedavailablegeneral-purposeprogramminglanguages,suchasassembly,C,orAda.Low-levellanguageswereprominentastheygivestrongandprecisecontrolovertheresources.Reactivesystemsoftenrunwithverylimitedmemoryandtheirreactiontimeneedstobestaticallyknown.General-purpose,low-levellanguagesquicklyshowedtheirlimits.Thelow-leveldescriptiontheyofferisveryfarfromthespecificationofthesystems,makingimplementationerrorproneandcertificationactivitiesverydifficult.Alargenumberofembeddedapplicationsaretargetingcriticalfunctions–fly-by-wiresystems,controlsystemsinnuclearpowerplants,etc.Assuch,theyhavetofollowconstraintsimposedbycertificationauthoritiesthatevaluatethequalityofadesignbeforeproductionuse,forexamplethestandardsDO-178BinavionicsandIEC-61508intransport.Betteradaptedlanguageswereneeded.Thefirstideawastoturntoconcurrentprogrammingmodel,withthegoalofgettingclosertothespecification.Indeed,reactivesystemsareinherentlyconcurrent:thesystemanditsenvironmentareevolvinginparallelandconcurrencyisthenat-uralwaytocomposesystemsfrommoreelementaryones.Unfortunately,traditionalmodelsofChapterpublishedinReal-TimeSystems:DescriptionandVerificationTechniques:TheoryandTools,vol.1,Editor:NicolasNavetandStephanMertz.ISTE2008(Hermespublisher)LaboratoireVERIMAG,CentreEquation,2,avenuedeVignate,38610GIERES,France.Email:Paul.Caspi@imag.frLRI,Universite´Paris-Sud11,91405Orsay,France.Email:Marc.Pouzet@lri.fr1
Figure1:AScadedesignconcurrencycomewithnumerousproblemsofsystemanalysis,nondeterminism,orcompilation.Thesemodelshavethereforebeenseldomusedindomainswheresecurityisaconcern.Moreover,evenifthegoalistogetclosertoaspecification,theobtainedmodelsarefarfromformalismstraditionallyusedbyengineers(suchascontinuouscontrolandfinitestatetransitionsystems).1.1.1TheSynchronousLanguagesCriticalindustries(e.g.,avionics,energy),drivenbyhighsecurityneeds,werethefirststoactivelyresearchnewdevelopmenttechniques.Ananswerwasproposedatthebeginningofthe80’swiththeintroductionofsynchronouslanguages[3],themostfamousofwhichareEsterel[5],Lus-tre[25]andSignal[4].Theselanguages,basedonamathematicalmodelofconcurrencyandtime,aredesignedexclusivelytodescribereactivesystems.Theideaofdedicatedprogramminglanguageswithalimitedexpressivepower,butperfectlyadaptedtotheirdomainofapplication,isessential.Thegainobtainedliesinprogramanalysisandtheabilitytooffercompile-timeguaran-teesontheruntimebehavioroftheprogram.Forexample,real-timeexecutionandtheabsenceofdeadlocksareguaranteedbyconstruction.Synchronouslanguageshavebeensuccessfullyappliedinseveralindustriesandhavehelpedinbringingformalmethodstoindustrialdevelopments.Synchronouslanguagesarebasedonthesynchronoushypothesis.Thishypothesiscomesfromtheideaofseparatingthefunctionaldescriptionofasystemfromtheconstraintsofthearchitec-tureonwhichitwillbeexecuted.Thefunctionalityofthesystemcanbedescribedbymakinganhypothesisofinstantaneouscomputationsandcommunications,aslongasitcanbeverifiedafterwardthatthehardwareisfastenoughfortheconstraintsimposedbytheenvironment.Thisistheclassicalzerodelaymodelofelectronicsorcontroltheory.Itpermitsreasoninginlogicaltimeinthespecification,withoutconsideringtherealtimetakenbycomputations.Underthesynchronoushypothesis,nondeterminismassociatedtoconcurrencydisappears,asthemachineissupposedtohaveinfiniteresources.Itispossibletodesignhigh-levelprogramminglanguagesthatfeatureparallelconstructions,butcanbecompiledtoefficientsequentialcode.Thecorrespon-dencebetweenlogicaltimeandphysicaltimeisverifiedbycomputingtheworstcasereactiontimeoftheprograms.Lustreisbasedontheideathattherestrictionofafunctionallanguageonstreams,similartoLucid[2]andtheprocessnetworkofKahn[32],wouldbewelladaptedtothedescriptionofreactivesystems.1Lustreisbasedonadata-flowprogrammingmodel.Asystemisdescribedasasetofequationsoversequences.Thesesequences,orflows,representsthecommunicationsbetweenthecomponentsofthesystem.Thisprogrammingmodelisclosetothespecificationsusedbyengineersofcriticalsoftwarethusreducingthedistancebetweenspecificationandimplementation.InLustre,thespecificationistheimplementation.Moreover,thelanguageisverywelladaptedtotheapplicationofefficienttechniquesforverification(seechapter6byPascalRaymond),test[43],1LustreisthecontractionofLucid,SynchroneetTempsRe´el—Lucid,SynchronousandReal-Time.2
Figure2:AChronometerinStateflow.andcompilation[26].TheadequationofthelanguagewiththedomainandtheefficiencyofthetechniquethatcanbeappliedonitpromptedtheindustrialsuccessofLustreandofitsindustrialversionScade[44].ScadeoffersagraphicalmodelingoftheLustreequations,closetothediagramsusedbycontrolorcircuitsdesigners(figure1).Scadecomeswithformalvalidationtoolsanditscodegeneratoriscertified(DO-178B,levelA),reducingtheneedfortesting.Asoftoday,Scadeisusedbynumerouscriticalindustries.ItisforexampleakeyelementinthedevelopmentofthenewAirbusA380.1.1.2ModelBasedDesignMeanwhile,non-criticalindustriescontinuedusinggeneralpurposelanguages,orlow-leveldedi-catedlanguages(normIEC-1131).Securityneedsweremuchloweranddidnotjustifythecostofchangingdevelopmentmethods.Itispushedbytheincreasingsizeandcomplexityofsystems,combinedwithaneedfordecreasingdevelopmentcyclesthattheyfinallylookedforothermethods.Itistherecentandmassiveadoptionofmodelbaseddevelopmentenvironments,thegrowinguseofSimulink/StateflowandtheappearanceofUML.Integratedenvironmentsofferadescriptionofsystemsusinghigh-levelgraphicalformalismsclosetoautomataordata-flowdiagrams.Theypro-videextensivesetsoftoolsforsimulation,test,orcode-generation.Again,thedistancebetweenspecificationandimplementationhasbeenreduced,thesystembeingautomaticallygeneratedfromthemodel.Thesetoolshaveusuallynotbeendesignedwithformaldevelopmentinmind.Theirsemanticsisoftenpartiallyandinformallyspecified.Thisisaseriousproblemforverificationorcertificationactivities.Itisalsoagrowingproblemforthedevelopmentactivityitself:thecomplexityofthesystemsincreasing,theriskofmisinterpretingthemodelsisalsoincreasing.AnexampleofsuchanenvironmentisSimulink/Stateflow[38](figure2)anindustrialde-factostandard.Simulink/Stateflowdoesnothaveaformalsemanticsanditispossibletowriteprogramsthatwillfailatruntime.Ontheotherhand,theenvironmentoffersacompletesetoftools,inwhichboththemodelanditsenvironmentcanbemodeled,simulatedandcodecanbeautomaticallygenerated.1.1.3ConvergingNeedsToday,theneedsofallindustriesdealingwithreactivesystems,criticalornot,areconverging.Theyareallfacingproblemsduetotheincreasingsizeandcomplexityofthesystems.Synchronouslanguages,createdtoanswertheneedsofspecificsdomains(forexamplecriticalsoftwareforLustre)arenotdirectlyadaptedtothedescriptionofcomplexsystemsmixingseveraldomains.Theneedsforverificationandsystemanalysis,foratimespecifictocriticalindustries,arenoweverywhere.Thesizeofthesystemsrequiresautomationofverificationortestgenerationactivities,3