Synchronous Functional Programming: The Lucid Synchrone Experiment

Paul Caspi

Description

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

Sujets

• Airbus
• Raymond
• System
• multiplication

Informations

• Publié par: pefav
• Nombre de lectures: 17
• Langue: English

Extrait

SynchronousFunctionalProgramming: TheLucidSynchroneExperiment ∗ PaulCaspi † Gre´goireHamonMarcPouzet ‡ VERIMAGTheMathWorksLRI,Univ.Paris-Sud11 GrenobleBostonOrsay 1Introduction LucidSynchrone isaprogramminglanguagededicatedtothedesignofreactivesystems.Itis basedonthesynchronousmodelof Lustre [25]whichitextendswithfeaturesusuallyfoundin functionallanguagessuchashigher-orderorconstructeddata-types.Thelanguageisequipped withseveralstaticanalysis,allexpressedasspecialtype-systemsandusedtoensuretheabsence ofcertainrun-timeerrorsonthefinalapplication.Itprovides,inparticular,automatictypeand clockinferenceandstaticallydetectsinitializationissuesordead-locks.Finally,thelanguageoffers bothdata-flowandautomata-basedprogramminginsideauniqueframework. Thischapterisatutorialintroductiontothelanguage.Itsaimistoshowthattechniquescan beapplied,atthelanguagelevel,toeasethespecification,implementation,andverificationof reactivesystems. 1.1ProgrammingReactiveSystems Weareinterestedinprogramminglanguagesdedicatedtothedesignofreactivesystems[31].Such systemsinteractcontinuouslywiththeirexternalenvironmentandhavetomeetstrongtemporal constraints:emergencybrakingsystems,planeautopilots,electronicstopwatches,etc.Inthe mid-70’s,withtheshiftfrommechanicalandelectronicsystemstologicalsystems,thequestion ofthecomputer-basedimplementationofreactivesystemsarose.Atfirst,theseimplementations usedavailablegeneral-purposeprogramminglanguages,suchasassembly, C ,or Ada .Low-level languageswereprominentastheygivestrongandprecisecontrolovertheresources.Reactive systemsoftenrunwithverylimitedmemoryandtheirreactiontimeneedstobestaticallyknown. General-purpose,low-levellanguagesquicklyshowedtheirlimits.Thelow-leveldescription theyofferisveryfarfromthespecificationofthesystems,makingimplementationerrorprone andcertificationactivitiesverydifficult.Alargenumberofembeddedapplicationsaretargeting criticalfunctions–fly-by-wiresystems,controlsystemsinnuclearpowerplants,etc.Assuch, theyhavetofollowconstraintsimposedbycertificationauthoritiesthatevaluatethequalityofa designbeforeproductionuse,forexamplethestandardsDO-178BinavionicsandIEC-61508in transport. Betteradaptedlanguageswereneeded.Thefirstideawastoturntoconcurrentprogramming model,withthegoalofgettingclosertothespecification.Indeed,reactivesystemsareinherently concurrent:thesystemanditsenvironmentareevolvinginparallelandconcurrencyisthenat- uralwaytocomposesystemsfrommoreelementaryones.Unfortunately,traditionalmodelsof ∗ ChapterpublishedinReal-TimeSystems:DescriptionandVerificationTechniques:TheoryandTools,vol.1, Editor:NicolasNavetandStephanMertz.ISTE2008(Hermespublisher) † LaboratoireVERIMAG,CentreEquation,2,avenuedeVignate,38610GIERES,France.Email: [e-mail] ‡ LRI,Universite´Paris-Sud11,91405Orsay,France.Email: [e-mail] 1

Figure1:A Scade design concurrencycomewithnumerousproblemsofsystemanalysis,nondeterminism,orcompilation. Thesemodelshavethereforebeenseldomusedindomainswheresecurityisaconcern.Moreover, evenifthegoalistogetclosertoaspecification,theobtainedmodelsarefarfromformalisms traditionallyusedbyengineers(suchascontinuouscontrolandfinitestatetransitionsystems). 1.1.1TheSynchronousLanguages Criticalindustries(e.g.,avionics,energy),drivenbyhighsecurityneeds,werethefirststoactively researchnewdevelopmenttechniques.Ananswerwasproposedatthebeginningofthe80’swith theintroductionofsynchronouslanguages[3],themostfamousofwhichare Esterel [5], Lus- tre [25]and Signal [4].Theselanguages,basedonamathematicalmodelofconcurrencyand time,aredesignedexclusivelytodescribereactivesystems.Theideaofdedicatedprogramming languageswithalimitedexpressivepower,butperfectlyadaptedtotheirdomainofapplication,is essential.Thegainobtainedliesinprogramanalysisandtheabilitytooffercompile-timeguaran- teesontheruntimebehavioroftheprogram.Forexample,real-timeexecutionandtheabsenceof deadlocksareguaranteedbyconstruction.Synchronouslanguageshavebeensuccessfullyapplied inseveralindustriesandhavehelpedinbringingformalmethodstoindustrialdevelopments. Synchronouslanguagesarebasedonthesynchronoushypothesis.Thishypothesiscomesfrom theideaofseparatingthefunctionaldescriptionofasystemfromtheconstraintsofthearchitec- tureonwhichitwillbeexecuted.Thefunctionalityofthesystemcanbedescribedbymaking anhypothesisofinstantaneouscomputationsandcommunications,aslongasitcanbeverified afterwardthatthehardwareisfastenoughfortheconstraintsimposedbytheenvironment.This istheclassicalzerodelaymodelofelectronicsorcontroltheory.Itpermitsreasoninginlogical timeinthespecification,withoutconsideringtherealtimetakenbycomputations.Underthe synchronoushypothesis,nondeterminismassociatedtoconcurrencydisappears,asthemachineis supposedtohaveinfiniteresources.Itispossibletodesignhigh-levelprogramminglanguagesthat featureparallelconstructions,butcanbecompiledtoefficientsequentialcode.Thecorrespon- dencebetweenlogicaltimeandphysicaltimeisverifiedbycomputingtheworstcasereactiontime oftheprograms. Lustre isbasedontheideathattherestrictionofafunctionallanguageonstreams,similarto Lucid [2]andtheprocessnetworkofKahn[32],wouldbewelladaptedtothedescriptionofreactive systems. 1 Lustre isbasedonadata-flowprogrammingmodel.Asystemisdescribedasaset ofequationsoversequences.Thesesequences,orflows,representsthecommunicationsbetween thecomponentsofthesystem.Thisprogrammingmodelisclosetothespecificationsusedby engineersofcriticalsoftwarethusreducingthedistancebetweenspecificationandimplementation. In Lustre ,thespecificationistheimplementation.Moreover,thelanguageisverywelladaptedto theapplicationofefficienttechniquesforverification(seechapter6byPascalRaymond),test[43], 1 Lustre isthecontractionofLucid,SynchroneetTempsRe´el—Lucid,SynchronousandReal-Time. 2

Figure2:AChronometerin Stateflow . andcompilation[26].Theadequationofthelanguagewiththedomainandtheefficiencyofthe techniquethatcanbeappliedonitpromptedtheindustrialsuccessof Lustre andofitsindustrial version Scade [44]. Scade offersagraphicalmodelingofthe Lustre equations,closetothe diagramsusedbycontrolorcircuitsdesigners(figure1). Scade comeswithformalvalidation toolsanditscodegeneratoriscertified(DO-178B,levelA),reducingtheneedfortesting.As oftoday, Scade isusedbynumerouscriticalindustries.Itisforexampleakeyelementinthe developmentofthenewAirbusA380. 1.1.2ModelBasedDesign Meanwhile,non-criticalindustriescontinuedusinggeneralpurposelanguages,orlow-leveldedi- catedlanguages(normIEC-1131).Securityneedsweremuchloweranddidnotjustifythecost ofchangingdevelopmentmethods.Itispushedbytheincreasingsizeandcomplexityofsystems, combinedwithaneedfordecreasingdevelopmentcyclesthattheyfinallylookedforothermethods. Itistherecentandmassiveadoptionofmodelbaseddevelopmentenvironments,thegrowinguseof Simulink / Stateflow andtheappearanceofUML.Integratedenvironmentsofferadescriptionof systemsusinghigh-levelgraphicalformalismsclosetoautomataordata-flowdiagrams.Theypro- videextensivesetsoftoolsforsimulation,test,orcode-generation.Again,thedistancebetween specificationandimplementationhasbeenreduced,thesystembeingautomaticallygenerated fromthemodel. Thesetoolshaveusuallynotbeendesignedwithformaldevelopmentinmind.Theirsemantics isoftenpartiallyandinformallyspecified.Thisisaseriousproblemforverificationorcertification activities.Itisalsoagrowingproblemforthedevelopmentactivityitself:thecomplexityof thesystemsincreasing,theriskofmisinterpretingthemodelsisalsoincreasing.Anexample ofsuchanenvironmentis Simulink / Stateflow [38](figure2)anindustrialde-factostandard. Simulink / Stateflow doesnothaveaformalsemanticsanditispossibletowriteprogramsthat willfailatruntime.Ontheotherhand,theenvironmentoffersacompletesetoftools,inwhich boththemodelanditsenvironmentcanbemodeled,simulatedandcodecanbeautomatically generated. 1.1.3ConvergingNeeds Today,theneedsofallindustriesdealingwithreactivesystems,criticalornot,areconverging. Theyareallfacingproblemsduetotheincreasingsizeandcomplexityofthesystems.Synchronous languages,createdtoanswertheneedsofspecificsdomains(forexamplecriticalsoftwarefor Lustre )arenotdirectlyadaptedtothedescriptionofcomplexsystemsmixingseveraldomains. Theneedsforverificationandsystemanalysis,foratimespecifictocriticalindustries,arenow everywhere.Thesizeofthesystemsrequiresautomationofverificationortestgenerationactivities, 3