IF Tutorial IF Tutorial

IF Tutorial Marius BOZGA Susanne GRAF Iulian OBER Laurent MOUNIER VERIMAG Distributed and Comp le x Systems Group www-verimag.imag.fr/PEOPLE/async/IF/ SPIN work sh op IF Tut o rial 1 A p ril 2, 200 4 mot i vat i on – l anguage – tools – c ase s t udies - p erspectives model based development Goal Early detection of problems, concerning functional and non functional aspects model-based simulation, testing and verification Context Telecommunication protocols, Real-time embedded systems, Distributed systems, Scheduling problems,… SPIN work sh op IF Tut o rial 2 A p ril 2, 200 4mot i vat i on – l anguage – tools – c ase s t udies - p erspectives approach: build on the existing User level modeling and CASE tools (SDL, UML, SCADE, …) Translation to a intermediate language, rich enough for modeling and for validation Optimisation a nd abstraction state Semantic model (state graph) explosion simulation verification3 verification1 test verification2 SPIN work sh op IF Tut o rial 3 A p ril 2, 200 4mot i vat i on – l anguage – tools – c ase s t udies - p erspectives approach: build on the existing CADP LOTOS guarded commands Optimisation a nd abstraction Semantic model (state graph) simulation verification3 verification1 test verification2 SPIN work sh op IF Tut o rial 4 A p ril 2, 200 4mot i vat i on – l anguage – tools – c ase s t udies - p erspectives approach: build on the existing Kronos Timed automata Optimisation a nd abstraction Semantic model (state graph) verification2 verification1 SPIN work sh op IF Tut o rial 5 A p ril 2, 200 4mot i vat i on – l anguage – tools – c ase s t udies - p erspectives challenge A good intermediate representation • S ufficient expressiveness : allows to map concepts of diverse modeling languages (asynchronous, synchronous, timing,…) • E nough concepts : structured representation of – C oncepts existing in validation tools – C oncepts exploitable for more efficient validation • A llows semantic fine tuning : allows expression of alternative options of semantic variation points: time progress, execution and interaction modes,… SPIN work sh op IF Tut o rial 6 A p ril 2, 200 4overview • M otivation and challenge • IF: the language concepts – F unctional aspects – N on-fu n ctional aspects • IF: the toolset – C ore components – M odel-based validation – F ront-end tools • D emos • Case studies • P erspectives SPIN work sh op IF Tut o rial 7 A p ril 2, 200 4mot i vation – language – tools – c ase s t udies - perspectives perspectives • U ML-based methodology for real-time systems – c omponent-based modeling – c ombination asynchronous and synchronous syste ms – r elate functional and non-functional aspects • i mprove verification and test generation methods – m ore static analysis , abstraction and constraint propagation – m ore compos itional verification methods – better diagnostics facilities • m ore connections – c onnections with performance evaluation tools SPIN work sh op IF Tut o rial 8 A p ril 2, 200 4The IF Language Functional Part SPIN work sh op IF Tut o rial 1 A p ril 2, 200 4system – p rocess – c ommunic a tion – example – e xtens ions IF Specification System description : 3 axes Processes extended timed automata IF (non-determinism, dynamic creation) predefined data types (basic types, arrays, Communications records) asynchronous channels abstract data types shared variables Data SPIN work sh op IF Tut o rial 2 A p ril 2, 200 4