Aniterative methodforthedesign processofmodehandling models
Genie Informatique · 2006
Thispaperdealswitha multilevel modular approach forthedesign process ofa modeldedicated to mode handling offlexible manufacturing systems. This model was proposedin our earlier work.It is characterized byastrong hierarchy andconcurrency thatiswhywithin thedesign process aniterative approach forspecification, verification andvalidation isintroduced in ordertoimprove thisprocess. Themainproperties being verified arepresented and theapproachisillustrated through anexample ofamanufacturing production cell. The formalanalysis toolsintegrated intothedevelopment environment Esterel Studio areusedwithin theproposed design process. According toourdesign approach offault tolerant control systems, modehandling isafunction ofsupervision. In viewofa disturbance (failures, breakdowns) mode handling allows implementing thedecisions about mode andconfiguration changing. Thedesign ofmodehandling function needstoprovide a modelrepresenting the operating modesoftheproduction systemandits subsystems. To thisaim,itisimportant tousean adequate modeling methodandpowerful specification formalism. We proposed inourearly workamodeling approach forreactive modehandling ofFlexible Manufacturing Systems (FMS)(HAM,05)(HAM, 06). Duetoincreasing complexity andflexibility ofFMS, someproblems canappearduring modechanging if coherence andsafety constraints arenottakeninto account inthespecification/modeling stages. Soitis necessary toverify andvalidate theproposed models at theearly stages ofthedesign process. A greater interest hasbeenallocated forfewyears toformal verification methods, whichguarantee that forallpossible evolutions ofamodel, several properties aresatisfied. Thepurpose ofthispaperistopresent aniterative approach forspecification andVerification & Validation (V&V)ofabehavioral modeldedicated toFMS mode handling. Thepaper isorganized asfollows. Insection II thebasic concepts ofV&V arereminded andthedesign process basedonformal methods isintroduced. The stages ofthis design process including V&V aredetailed insection IIIandsection IV.Theiterative approach is presented andthemainproperties being verified within thisprocess arepresented. Finally theapproach is illustrated using anexample ofaflexible manufacturing cell.