Proceedings of the 5th Workshop of the MPM4CPS COST Action

COST Action IC1404: Multi-Paradigm Modelling for Cyber-Physical Systems http://www.mpm4cps.eu/ Proceedings of the 5th Workshop of the MPM4CPS COST Action November 24-25, 2016  Malaga, Spain Hans Vangheluwe, Vasco Amaral, Holger Giese, Jan Broenink, Bernhard Schätz, Alexander Norta, Paulo Carreira, Miguel Goulão, Antonio Vallecillo, Tanja Mayerhofer (Eds.) Technical Report No. ITI16/02 Departamento de Lenguajes y Ciencias de la Computación. Universidad de Málaga. Copyright © 2016 for the individual papers by the papers' authors. Copying permitted for private and academic purposes. This volume is published and copyrighted by its editors. Editors: Hans Vangheluwe University of Antwerp (Belgium) Vasco Amaral Universidade Nova de Lisboa (Portugal) Holger Giese Hasso-Plattner-Institut für Softwaresystemtechnik GmbH (Germany) Jan Broenink University of Twente (Netherlands) Bernhard Schätz fortiss GmbH (Germany) Alexander Norta Tallinn University of Technology (Estonia) Paulo Carreira Universidade de Lisboa (Portugal) Miguel Goulão Universidade Nova de Lisboa (Portugal) Antonio Vallecillo Universidad de Málaga (Spain) Tanja Mayerhofer TU Wien (Austria) Table of Contents Preface............................................................................ I Foundations Modeling Mobility Using Dynamic Topology Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1–21 Fernando J. Barros EngineeringHybridModellingLanguages ........................................... 22–34 Sadaf Mustafiz, Cláudio Gomes, Bruno Barroca, Hans Vangheluwe Real-TimeMDE:AnOverview ..................................................... 35–46 Moussa Amrani, Pierre-Yves Schobbens Novel Verification Paradigms for Nonlinear Hybrid Automata . . . . . . . . . . . . . . . . . . . . . . . . . . 47–55 Eva M. Navarro López Usability Driven Development with Usability Software Engineering Modeling Environment (USE-ME) ........................................................................ 56–75 Ankica Bariši´c Automated Analysis of Traceability in Cyber-Physical Systems (Tool Demonstration) . . . . 76–92 Ferhat Erata, Bedir Tekinerdogan Techniques A Hybrid Master (Discrete-Event and Discrete-Time) for Functional Mockup Interface . . . 93–100 Vincent Albert Adding Uncertainty and Units to Quantity Types in Software Models . . . . . . . . . . . . . . . . . . . 101–110 Loli Burgueño, Tanja Mayerhofer, Antonio Vallecillo, Manuel Wimmer Integrating Uncertainty Modelling with Use Case Modelling to Discover Unknowns . . . . . 111–117 Tao Yue, Shaukat Ali, Man Zhang Model-Driven Testing of Cyber-Physical Systems with the Explicit Consideration of Uncertainty(U-Testing) ............................................................ 118–123 Shaukat Ali, Man Zhang, Tao Yue Separation of Concerns in Continuous Time Hierarchical Co-Simulation . . . . . . . . . . . . . . . . 124–130 Cláudio Gomes, Joachim Denil, Bart Meyers, Hans Vangheluwe Modeling of Cooperation Behavior in Flexible Vehicle Platoon Based on Hybrid Automaton andPredicitiveAnalysis ............................................................ 131–142 Lejla Banjanovic-Mehmedovic Introduction to Physical-Systems Modelling with Bond Graphs (Tutorial) . . . . . . . . . . . . . . . 143–159 Jan F. Broenink Application Domains Architecting the Next Generation of Vehicles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160–174 Patrizio Pelliccione Innovative Designs through Topological Design Space Exploration . . . . . . . . . . . . . . . . . . . . . 175–191 Mike Nicolai Simulation and Design-Time Analysis of the Smart Grid in the Czech Republic . . . . . . . . . . 192–195 Barbora Buhnova A Multi-Domain Approach to Design of CPS in Special Education: Issues of Evaluation andAdaptation(Paper) ............................................................. 196–205 Maya Dimitrova, Anna Lekova, Snezhanka Kostova, Chavdar Roumenin, Milena Cherneva, Aleksandar Krastev, Ivan Chavdarov Education How to Exploit an Experience Gained in CPS Related Projects for Master Students Training PrograminERASMUS+Project .................................................... 206-221 Anatolijs Zabašta, Nadezda Kun ,icina, Oksana Nikiforova, Andrejs Romanovs Preface In virtually any area of human activity, Cyber-Physical Systems (CPS) are emerging. CPS are truly complex, designed systems that integrate physical, software and network aspects. To date, no unifying theory and no systematic design methods, techniques and tools exist for such systems. Individual mechanical, electrical, network or software engineering disciplines only offer partial solutions. Multiparadigm Modelling (MPM) proposes to model every part and aspect of a system explicitly, at the most appropriate level(s) of abstraction, using the most appropriate modelling formalism(s). Modelling language engineering, including model transformations, and the study of their semantics, are used to realize MPM. MPM is seen as an effective answer to the challenges of designing CPS. The COST Action IC1404: Multi-Paradigm Modelling for Cyber-Physical Systems (MPM4CPS) aims to promote foundations, techniques and tools for multi-paradigm modelling for cyber-physical systems, and to provide educational resources to both academia and industry. This will be achieved by bringing together and disseminating knowledge and experiments on CPS problems and MPM solutions. The fifth MPM4CPS workshop took place on November 24-25, 2016 in Malaga, Spain. The program comprised presentations of MPM4CPS COST Action members discussing their work on foundations, techniques, application domains, and education in MPM4CPS, as well as joint work meetings. These proceedings collect the presentations given at the workshop. They cover many different aspects of multi-paradigm modelling for cyber-physical systems including, but not limited to – foundations of MPM4CPS including –language engineering, –model transformations, –verification paradigms, –traceability; – techniques in MPM4CPS including –co-simulation, –uncertainty modelling, –model-driven testing, –predictive analysis; – application domains of MPM4CPS in the –automotive industry, –aviation industry, –smart grids, –robotics; – education in MPM4CPS. We would like to thank the presenters contributing their work to the MPM4CPS COST Action. Furthermore, we would like to thank Antonio Vallecillo, Loli Burgueño and Tanja Mayerhofer for organizing the workshop. December 2016 I 0RGHOLQJ0RELOLW\XVLQJ'\QDPLF 7RSRORJ\0RGHOV )HUQDQGR-%DUURV 'HSW,QIRUPDWLFV(QJLQHHULQJ 8QLYHUVLW\RI&RLPEUD 3RUWXJDO 0DODJD6SDLQ1RYHPEHU IC1404 – Multi-Paradigm Modelling for Cyber-Physical Systems 7KHUHSUHVHQWDWLRQRIVSDWLDOO\PRYLQJHQWLWLHVLV FRPPRQO\DFKLHYHGXVLQJSXEOLVKVXEVFULEH FRPPXQLFDWLRQ36& 36&FDQEHFRPHFRPSOH[DQGLQHIILFLHQW UHTXLUHVWKHGHILQLWLRQRIUHJLRQVRILQWHUHVW JHQHUDWHVIDOVHSRVLWLYHPHVVDJHV &RQYHQWLRQDOVWDWLFSHHUWRSHHU FRPPXQLFDWLRQ33&WKRXJKXVXDOO\PRUH HIILFLHQWGRHVQRWKDYHWKHUHTXLUHGIOH[LELOLW\WR UHSUHVHQWPRELOHHQWLWLHV ,QWURGXFWLRQ 1 :HKDYHGHYHORSHGWKHLQWHJUDWLRQRI36&DQG 33&VW\OHVXQGHUWKHKLHUDUFKLFDODQGPRGXODU G\QDPLFWRSRORJ\SDUDGLJP 7KHXQLILFDWLRQLVDFKLHYHGXVLQJUXQWLPH WRSRORJ\DGDSWDWLRQ O,WLQYROYHVWKHG\QDPLFFUHDWLRQGHOHWLRQRI OLQNVWRFDSWXUHWKHFXUUHQWLQWHUDFWLRQV EHWZHHQHQWLWLHV 7KHDUFKLWHFWXUHFRPELQHVWKHDGYDQWDJHVRI 36&DQG33&HQDEOLQJDIOH[LEOHVLPXODWLRQ DUFKLWHFWXUH ,QWURGXFWLRQ 7KHDUFKLWHFWXUHVXSSRUWVWZRW\SHVRI36& VW\OHV WKHWUDGLWLRQDOSXVKVW\OHoHYHQWV WKHQRYHOSXOOVW\OHoVDPSOLQJ DEVWUDFWVLQIRUPDWLRQUHTXHVWDQGLQIRUPDWLRQ VHQGLQJ HQDEOHVH[DUDGDUWRVDPSOHDWLWVRZQUDWH %HQHILWVDUHGHPRQVWUDWHGWKURXJKWKHPRGHOLQJ RIDQDLUGHIHQVHVFHQDULRGHVFULEHGLQWKH +\)ORZ PRGHOLQJDQGVLPXODWLRQIUDPHZRUN ,QWURGXFWLRQ 2 3XVK&RPPXQLFDWLRQ 3XOO&RPPXQLFDWLRQ 3 7KH+LJK/HYHO$UFKLWHFWXUH+/$LVD VWDQGDUGIRU06 +/$LVEDVHGRQSXEOLVKVXEVFULEH FRPPXQLFDWLRQ36& +/$HQDEOHVWKHLQWHURSHUDELOLW\RIVLPXODWRUV WRFUHDWHFRPSOH[VFHQDULRV +/$VXSSRUWVIHGHUDWHVDQGIHGHUDWLRQVD FRPELQDWLRQRIIHGHUDWHV +/$2YHUYLHZ +/$REMHFWVFDQEHXVHGWRDFKLHYHWKH FRPPXQLFDWLRQWKURXJKVKDUHGPHPRU\ +/$REMHFWVDUHSDVVLYHHQWLWLHVGHSHQGLQJRQ IHGHUDWHVWREHPRGLILHG 7KHIHGHUDWHVLQYROYHGLQ+/$REMHFW PDQDJHPHQWDQGLQIRUPDWLRQUHWULHYDOKDYHWKHLU UHXVHVHYHUHO\OLPLWHG +/$2YHUYLHZ 10 +/$57,FDQQRWEHPRGLILHG QRVXSSRUWIRU33& +/$VXSSRUWVRQO\IODWPRGHOV FRPSOH[PRGHOVEHQHILWIRUPDKLHUDUFKLFDO UHSUHVHQWDWLRQ +/$LPSRVHV36& 33&FDQSURYLGHDEHWWHUUHSUHVHQWDWLRQ +/$LVEDVHGRQWKHGLVFUHWHHYHQWSDUDGLJP KRZWRUHSUHVHQWFRQWLQXRXVPRGHOV" PRYLQJHQWLWLHV" +/$/LPLWDWLRQV 3XEOLVKVXEVFULEHRSHUDWLRQVSURYLGHDQ DEVWUDFWLRQIRUGHVFULELQJG\QDPLFWRSRORJLHV 1HZFRPSRQHQWVFDQEHDGGHGUHPRYHG G\QDPLFDOO\WRIURPDQHWZRUNZLWKRXWDIIHFWLQJ WKHH[LVWLQJFRPSRQHQWV 33FRPPXQLFDWLRQLVPRUHHIILFLHQWIRU UHSUHVHQWLQJNQRZQOLQNV QRIDOVHSRVLWLYHPHVVDJHV UHTXLUHVQRILOWHUV 2XUVROXWLRQ 8VHG\QDPLF33&WRUHSUHVHQW36& &RPELQLQJ33ZLWK36& 11 &RPELQLQJ33ZLWK36& 7RSRORJ\FDQEHGHVFULEHGLQDFRPSDFWPDQQHU E\EXONFRPPDQGV 'URQH'URQH SXEOLVK&)[\ SXEOLVK')FRPP 5DGDU VXEVFULEH&)[\ VXEVFULEH')FRPP %XONFRPPDQGVFDQEHPDSSHGLQWR33&OLQNV LQ-8VH+\)ORZ 3URYLGHVWKHXQLILFDWLRQRI36&DQG33& &RPELQLQJ33ZLWK36& 12 ,QPDQ\PRGHOVZHZDQWWROLQNHQWLWLHVWKDWDUH NQRZQWRLQWHUDFW 3XUVXHUGURQH $SXUVHULVRQO\FRQQHFWHGWRRQHWDUJHW ZK\XVLQJ36&" 5DGDUGURQH $FFXUDWHGHWHFWLRQUHTXLUHVDGDSWLYH VDPSOLQJGHSHQGLQJRQEHDPGURQH GLVWDQFH +\)ORZ H[HFXWLYHFDQFUHDWHG\QDPLFOLQNVWR VXSSRUW33&FRPPXQLFDWLRQ &RPELQLQJ33ZLWK36& &RPELQLQJ33ZLWK36& 13 6SDWLDOSDUWLWLRQLQJFDQEHLQWHJUDWHGZLWK33& LQRUGHUWRDFKLHYHDQHIILFLHQWGHVFULSWLRQRI PRELOHHQWLWLHV :HFRQVLGHUDUHJLRQRILQWHUHVW52,PDQDJHU FRPSRQHQWZLWKWKHDELOLW\WRNHHSWUDFNRI SXEOLVKVXEVFULEH (QWLWLHVFDQGHFODUH52,VWRWKHPDQDJHU ZKHQWKHVHUHJLRQVRYHUODSWKLVFRPSRQHQW VHQGVDVLJQDOWRWKHH[HFXWLYHWKDWFDQDGDSW WKHWRSRORJ\ $LU'HIHQVH $LU'HIHQVH 14 52,V 52,V 15 3HHUWR3HHU&RPPXQLFDWLRQ 52,V 16 $VHQWLWLHVPRYHWKHLUUHJLRQVRILQWHUHVWZLOO HYHQWXDOO\RYHUODS 7KHPDQDJHUXSRQRYHUODSGHWHFWLRQVHQGVD UHTXHVWWRWKHH[HFXWLYHWKDWZLOOFUHDWHDOLQN EHWZHHQWKHUDGDUDQGWKHGURQHVRLWFDQEH WUDFNHG 'URQHFDQQRWEHXVHGLQFRQYHQWLRQDOSXEOLVK VXEVFULEHFRPPXQLFDWLRQVLQFHLWVLQWHUIDFHGRHV QRWPDWFKUDGDUVDPSOLQJSRUW[\ 'URQHSRUW[\0LFRQYH\VWKHSRVLWLRQLQPLOHV ZKLOHWKHUDGDUUHTXLUHVWKLVLQIRUPDWLRQLQNP $LU'HIHQVH 7KHFRPPXQLFDWLRQEHWZHHQWKHUDGDUDQG 'URQHLVHVWDEOLVKHGE\WKH-8VH+\)ORZ FRPPDQG link("Radar","xy","Drone-4", "xyMi", x->x, mi->[1.61*mi[0],1.61*mi[1]]) $LU'HIHQVH 17 $LU'HIHQVH +\)ORZ G\QDPLFSHHUWRSHHUFRPPXQLFDWLRQLV DEOHWRUHSUHVHQWSXEOLVKVXEVFULEH FRPPXQLFDWLRQ ,WFDQDOVRUHSUHVHQWWKHVSDFHSDUWLWLRQLQJ DOJRULWKPVUHTXLUHGWRREWDLQDQHIILFLHQW UHSUHVHQWDWLRQRIPRYLQJHQWLWLHV $GGLWLRQDOO\SHHUWRSHHUOLQNVFDQEH HVWDEOLVKHGXVLQJ-8VH+\)ORZ DGDSWHU FDSDELOLWLHV $LU'HIHQVH 18 6FHQDULRZLWKWZRDLUERUQHUDGDUV5DQG5 PRYLQJDWFRQVWDQWYHORFLWLHVZLWKIL[HGUDGLXV WUDMHFWRULHV 7ZRGURQHV'DQG'PRYLQJDWDFRQVWDQW YHORFLW\EXWZLWKDSLHFHZLVHFRQVWDQWUDGLXV WKDWFKDQJHVDWUDQGRPWLPHV 7KHUDGDUVDUHPRGHOHGE\WKHLUURWDWLQJEHDPV WKDWKDYHDIL[HGSHULRG $UDGDUHFKRLVSURGXFHGZKHQDUDGDUEHDP GHWHFWVDGURQH $LU'HIHQVH 7KHVHLQWHUDFWLRQVUHTXLUHVWKHFUHDWLRQRIDQHZ GHWHFWRUIRUHDFKGURQH LWEHQHILWVIURP33&WRHQDEOHWKHGHWHFWRU WRVDPSOHWKHSRVLWLRQLQIRUPDWLRQIURPERWK WKHUDGDUEHDPDQGIURPDVSHFLILFGURQH 8SRQGHWHFWLRQUDGDUVFDQODXQFKDSXUVXHUWR GLVDEOHWKHGURQH 3XUVXHUVKDYHDGLJLWDOFRQWUROOHUWKDWXVHVD SURSRUWLRQDOODZIRUJXLGDQFH $LU'HIHQVH 19 $%5?$= )% $%5?'E(J>      +)  ') ; '  J' E(  26 $%5?'E( )% &6) )%  6K    )6 %H6 %H6 27 %&6) )% "  %   HL%>6%&6) )%? +6B$56+ )C$=D 3A+;3 42+342+4B5346#?+$,0C$-)1+'(#? 28 HL%>6%&6) )%? +6B$56+ )C'E(D D 42+"342+B5346#.+-)(/-),1+'(#. > 6,? $=C"?$=@ ?'E(D 2#H##  29 M5N#? ( ;?0  )3O $=C"D6) )% =8 %  /  53 !314E(-+?0-C.($ 0%")3 C6%"#;&D 30 M5N#? & > 68? 'E(C"?'E(@ ?$=D $%  31 M5N#? ( ;?0  )3O 'E(C"D6) )% 0%")3C6%"#;&D 32 M5N#? & 0&6) 3CDE  P % )%% 6) C;%)6#" PD %)  6 )% =  66C) %D %") E AAA  ###A AH";AB 33 EM5 =;60)370%")3 E   "A 66 ) E 'E( $= = %% 6)=) %% Q  34 www.unamur.be 5HDO7LPH0'( $Q2YHUYLHZ 0RXVVD$05$1,3LHUUH<YHV6&+2%%(16 &RVW $FWLRQ,& 030&36:RUNVKRS 0iODJD 6SDLQ± 7KXUVGD\ 1RYHPEHU  www.unamur.be 2 On a New Project… 35 www.unamur.be 15 Time Representation [1] [TaD]: Time as Data Time information represented within the model Example: clock counters, timers as MM attributes [TaC]: Time as Control Time information integrated at transformation level Example: time manipulation constructs available in the TL [TaE]: Time as Embedding Time not explicitly available Implicit in a third-party language, when translated Requires both model and transformation(s) to become translatable Not mutually exclusive: all three can be mixed!  >@ -'H/DUD(*XHUUD$%RURQDW5+HFNHODQG37RUULQL 'RPDLQ6SHFLILF 'LVFUHWH (YHQW0RGHOOLQJ DQG6LPXODWLRQ8VLQJ *UDSK7UDQVIRUPDWLRQ Journal of Software and Systems Modelling± www.unamur.be 16 CONTRIBUTIONS OVERVIEW 42 www.unamur.be 17 Overview & Choices 7LPH5HSUHVHQWDWLRQ 7UDQVIRUPDWLRQ /DQJXDJH 7/ 7LPH 7UDQVIRUPDWLRQ /DQJXDJH 7/ 7LPH5HSUHVHQWDWLRQ Contributions number 5 supporting references (classification, etc.) 40 overviewed contributions Space constraints Some are cited by website (one ref for 10 pubs) Others have several references for slightly different usage Presentation Choice Also related to space constraints First try: by time representation, but does not fit Finally: by TL Statistics By Transformation Language MPL GBT 18 By Time Domain Discrete Continuous Hybrid By Synchronicity Synchronous Asynchronous Hybrid By Communication Style Resource Sharing Message Passing 43 www.unamur.be 19 Summary Tables: MPLs Contribution Domain Language Features Time Rep. StateCharts Discrete Branching / Non-Determ. Asynch. / MPTaC Activity Diags fUML Discrete Branching / Non-Determ. Asynch. / MPTaC MARTE / CCSL Hybrid Branching / Non-Determ. Hybrid / ?? TaD + TaC HybridUML Hybrid Branching / Non-Determ. Asynch. / RSTaD + TaC ForSyDe Hybrid Branching / Non-Determ. Asynch. / RSTaC ModHel’X Hybrid Branching / Non-Determ. Hybdrid / MPTaC GeMoC Hybrid Branching / Non-Determ. Hybrid / ?? TaC 6\QFKURQLFLW\ KLLW &RPPXQLFDWLRQ Asynchronous Message-Passing Resource SharingResource S ge - Passin g Synchronous Hybrid Synchron chronous ybr i )HDWXUHV www.unamur.be 20 Summary Tables: GBTLs Contribution Domain Language Features Time Rep. Petri Nets Discrete Branching / Non-Determ. Asynch. / RSTaC Stochastic Hybrid Branching / Non-Determ. Asynch. / MPTaC De Lara & Vangheluwe Discrete Branching / Non-Determ. Asynch. / Rs TaC De Lara, Guerra et al. Hybrid Branching / Non-Determ. Asynch. / MPTaD + TaE Strobl et al. Discrete Branching / Non-Determ. Asynch. / RSTaD Gapay et al. Discrete Branching / Non-Determ. Asynch. / Rs TaD Moment 2 Discrete Branching / Non-Determ. Asynch. / Rs TaC E-Motions Discrete Branching / Non-Determ. Asynch. / Rs TaC MechatronicUML Hybrid Branching / Non-Determ. Asynch. / MPTaC ATOMPM Discrete Branching / Non-Determ. Asynch. / Rs TaE 6\QFKURQLFLW\ C E KLLW &RPPXQLFDWLRQ Asynchronous Message-Passing Resource SharingResource S ge - P assin g Synchronous Hybrid Synchron chro nous ybri )HDWXUHV 44 www.unamur.be 21 CONCLUSIONS www.unamur.be 22 Paper Summary 1. A Classification for studying Real-Time MDE contributions Which Transformation Language is used? Which characteristics of time are important for V&V? How time is represented in MDE Frameworks? 2. A partial validation on selected contributions 43 papers so far 3. An approach that should be refined, precised and extended Dimension 3 (Time Representation) should be more precise Is there more contribution in the « pure » MDE scope? How these compare with classical GPL approaches for time? (Ptolemy, DEVS, RT-Maude, but also Java, C, Ada, etc.) 45 www.unamur.be 23 Future Work 1. How to gather more papers? Perform a Systematic Litterature Review? Proceed by experience? (contact specialised researchers + my own) Extend the study’s scope? 2. Consider all possible V&V techniques for Real-Time Integrated Testing (i.e. with HW)iscommonfor embedded systems Simulation for continuous systems is also a huge domain Formal Verification is limited to very specific part in the whole system 46 Novel verification paradigms for nonlinear hybrid automata Several application domains Eva M. Navarro López School of Computer Science, Manchester, UK COST Action IC1404 – Multi-Paradigm Modelling for Cyber-Physical Systems (MPM4CPS) Málaga Workshop, WG1 Foundations Málaga, 24th November, 2016 The hybrid system salad DYVERSE: a modelling, verification and control framework Branches of DYVERSE Summary 1The hybrid system salad 2DYVERSE: a modelling, verification and control framework 3Branches of DYVERSE Eva Navarro López DYVERSE 47 The hybrid system salad DYVERSE: a modelling, verification and control framework Branches of DYVERSE The hybrid system recipe The hybrid system salad: A new fresh perspective Different labels for the same idea Combination of continuous dynamics and discrete phenomena Eva Navarro López DYVERSE The hybrid system salad DYVERSE: a modelling, verification and control framework Branches of DYVERSE DYVERSE: a cocktail of disciplines Hybrid automaton framework Research that challenges orthodoxy Mixing theory and practice, breaking boundaries of different disciplines DYnamical-driven VERification of Systems with Energy considerations The first-funded project in the UK on the verification and control of nonlinear hybrid systems Eva Navarro López DYVERSE 48 The hybrid system salad DYVERSE: a modelling, verification and control framework Branches of DYVERSE DYVERSE: a cocktail of disciplines Hybrid automaton framework Hybrid automaton framework: basic elements Eva Navarro López DYVERSE The hybrid system salad DYVERSE: a modelling, verification and control framework Branches of DYVERSE DyverseRBT: automated generation of hybrid automata DyverseBMC: falsification of safety properties Verification of liveness properties A collage of ideas Dynamically-aware abstractions and formal verification: exploiting dynamical properties of systems Application-oriented approach: results for real-world systems and automatic generation of hybrid automata from a dynamical specification Verification of stability-related and liveness properties Complex systems applications Eva Navarro López DYVERSE 49 The hybrid system salad DYVERSE: a modelling, verification and control framework Branches of DYVERSE DyverseRBT: automated generation of hybrid automata DyverseBMC: falsification of safety properties Verification of liveness properties Automated verification as a dynamical analysis tool Eva Navarro López DYVERSE The hybrid system salad DYVERSE: a modelling, verification and control framework Branches of DYVERSE DyverseRBT: automated generation of hybrid automata DyverseBMC: falsification of safety properties Verification of liveness properties DyverseRBT: Dyverse Rigid Body Toolbox What? To generate automatically a general-purpose transition system for the description of mechanical systems with multiple impacts and friction Why? Simulation: To create event-driven simulations of multi-rigid-body mechanical systems Formal verification: Hybrid systems automated verification tools to check that properties of mechanical systems are satisfied Control: To include formal verification results in the control loop to modify system response. Avoid ‘something bad will never happen’ (safety), ensure ‘something good will happen’ (liveness) Eva Navarro López DYVERSE 50 The hybrid system salad DYVERSE: a modelling, verification and control framework Branches of DYVERSE DyverseRBT: automated generation of hybrid automata DyverseBMC: falsification of safety properties Verification of liveness properties Limitations in multi-contact rigid-body systems Beyond the bouncing ball A simple example that cannot be expressed using the classical hybrid automaton framework Eva Navarro López DYVERSE The hybrid system salad DYVERSE: a modelling, verification and control framework Branches of DYVERSE DyverseRBT: automated generation of hybrid automata DyverseBMC: falsification of safety properties Verification of liveness properties The multi-rigid-body (MRB) hybrid automaton Typical hybrid automaton elements Dynamical discrete locations Continuous states Initial states Continuous dynamics Domains of discrete locations Edges (discrete transitions) Guards Reset maps New elements integrating computation of contact forces Computation nodes Non-dynamical discrete locations Eva Navarro López DYVERSE 51 '6//LIHF\FOH $QNLFD%DULãLü ϳ9«ėÏá³đ̺ qIĄÏÆÌđɑ 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( '6//LIHF\FOH $QNLFD%DULãLü ϳ9«ėÏá³đ̺ qIĄÏÆÌđɑ ϳ9 «ėÏá³đ̺ ĄÏÆÌđ qIɑ 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 58 4XDOLW\LQ8VHLH8VDELOLW\ $QNLFD%DULãLü Ɣ 'LIIHUHQWODQJXDJHV OLNHO\KDYHGLIIHUHQW FRQWH[WVRIXVH Ɣ 7KHLUXVHUVDUHOLNHO\ WRKDYHGLIIHUHQW NQRZOHGJHVHWV Ɣ $PLQLPXPVHWRI RQWRORJLFDOFRQFHSWV LVUHTXLUHGWRXVHWKH ODQJXDJH 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( $QNLFD%DULãLü 8VDELOLW\6RIWZDUH(QJLQHHULQJ0RGHOLQJ(QYLURQPHQW 86(0( 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 59 $QNLFD%DULãLü  8VDELOLW\6RIWZDUH(QJLQHHULQJ0RGHOLQJ(QYLURQPHQW 86(0( 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 86(0(LQ'6/OLIHF\FOH $QNLFD%DULãLü  8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 60 86(0(LQ'6/OLIHF\FOH  $QNLFD%DULãLü 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( $QNLFD%DULãLü  &RQWH[W0RGHOLQJ86(0( 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 61 $QNLFD%DULãLü  8VHU+LHUDUFK\ 9LVXDOLQR 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( $QNLFD%DULãLü  9LVXDOLQR 8VHU7HPSODWHV 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 62 $QNLFD%DULãLü  &RQWH[W0RGHOLQJ86(0( 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( $QNLFD%DULãLü  9LVXDOLQR &RQWH[W(QYLURQPHQW 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 63 $QNLFD%DULãLü  &RQWH[W0RGHOLQJ86(0( 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( $QNLFD%DULãLü  9LVXDOLQR :RUNIORZV 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 64 $QNLFD%DULãLü  9LVXDOLQR 6FHQDULRV 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 86(0(LQ'6/OLIHF\FOH  $QNLFD%DULãLü 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 65 $QNLFD%DULãLü  *RDO0RGHOLQJ86(0( 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( $QNLFD%DULãLü  9LVXDOLQR 8VDELOLW\*RDO0RGHO 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 66 $QNLFD%DULãLü  *RDO0RGHOLQJ86(0( 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( $QNLFD%DULãLü  9LVXDOLQR 8VDELOLW\0HWKRGDQG 5HTXLUHPHQWV 9 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 67 $QNLFD%DULãLü  &RYHUDJH(QJLQH86(0( 8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 3XEOLFDWLRQV Â [XQE< <gQãQü 6<hE] Z<g<Y !QOkIY ]kY@] <[G GIZ<g OkQ<g ±[jg]GkEQ[O kh<DQYQjs E][EIg[h I<gYs Q[ jPI /  GIpIY]dZI[j EsEYI Y]q/ IrdIgQI[EIgId]gj±[+g]EIIGQ[Oh]NjPIÂhj[jIg[<jQ][<Y7]gXhP]d][!]GIYgQpI[IpIY]dZI[j+g]EIhhIh<[G+g<EjQEIh<jjPI ÂÈjP[jIg[<jQ][<Y!] /][NIgI[EI6<YI[EQ</d<Q[$Ej]DIgÃÁÂÅ Ã [XQE<<gQãQü±p<Yk<jQ[OjPI-k<YQjsQ[1hI]N]Z<Q[/dIEQNQE <[Ok<OIhQ[<[OQYI7<s±[+g]EIIGQ[Oh]NjPI]Ej]g<Y/sZd]hQkZ <jjPIÂÇjP[jIg[<jQ][<Y][NIgI[EI][!]GIYgQpI[[OQ[IIgQ[O <[Ok<OIh<[G/shjIZh¥!] /¦!Q<ZQY]gQG<1/1.$Ej]DIg ÃÁÂÄ Ä [XQE<<gQãQü±jIg<jQpIIp<Yk<jQ][]N]Z<Q[/dIEQNQE <[Ok<OIh±[+g]EIIGQ[Oh]NjPI!/jkGI[j.IhI<gEP]ZdIjQjQ][<jjPIÂÇjP [jIg[<jQ][<Y][NIgI[EI][!]GIYgQpI[[OQ[IIgQ[O <[Ok<OIh<[G/shjIZh¥!] /¦!Q<ZQY]gQG<!$Ej]DIgÃÁÂÄ Å [XQE<<gQãQü+IGg]!][jIQg]6<hE]Z<g<Y!QOkIY]kY@]!QOkIY!][jIQg]±+<jjIg[hN]gp<Yk<jQ[O1h<DQYQjs]N]Z<Q[/dIEQNQE <[Ok<OIh±[+g]EIIGQ[Oh]NjPIÂÊjP][NIgI[EI][d<jjIg[Y<[Ok<OIh]Ndg]Og<Zh¥+ ]+¦/+ /ÃÁÂÃ0kEh][gQv][<1/$Ej]DIg ÃÁÂà Æ gk[]<gg]E<Gk<gG]!<gfkIh6<YjIg<YIO<h6<hE]Z<g<Y<[G[XQE<<gQãQü±0PI.+/ <E<hIhjkGs]NY<[Ok<OII[OQ[IIgQ[O khQ[O!N]gI[Ig<jQ[O.+<ZIhN]g!]DQYI+P][Ih±[+g]EIIGQ[Oh]NjPIÂÃjP7]gXhP]d][]Z<Q[/dIEQNQE!]GIYQ[O<j/+ / ÃÁÂÃ0kEh][gQv][<!$Ej]DIgÃÁÂà Ç [XQE< <gQãQü 6<hE] Z<g<Y <[G !QOkIY ]kY@] ±1h<DQYQjs p<Yk<jQ][ ]N ]Z<Q[/dIEQNQE <[Ok<OIh± [+g]EIIGQ[Oh ]N jPI // ]Ej]g<Y/sZd]hQkZ<jjPIÉjP[jIg[<jQ][<Y][NIgI[EI][jPI-k<YQjs]N[N]gZ<jQ][<[G]ZZk[QE<jQ][h0IEP[]Y]Os¥-10¦ QhD][ +]gjkO<Y/IdjIZDIgÃÁÂÃ È [XQE<<gQãQü6<hE]Z<g<Y!QOkIY]kY@]<[Ggk[]<gg]E<±p<Yk<jQ[OjPI1h<DQYQjs]N]Z<Q[/dIEQNQE <[Ok<OI±[]]X]gZ<Y <[G+g<EjQE<YhdIEjh]N]Z<Q[/dIEQNQE <[Ok<OIh.IEI[jIpIY]dZI[jhIGQjIGDs!<gW<[!Ig[QXY]D<Y/IdjIZDIgÃÁÂÃd<OIh ÄÉÇÅÁÈ É [XQE< <gQãQü 6<hE] Z<g<Y !QOkIY ]kY@] <[G gk[] <gg]E< ±-k<YQjs Q[ 1hI ]N ]Z<Q[/dIEQNQE <[Ok<OI < <hI /jkGs± [+g]EIIGQ[Oh ]N jPI 7]gXhP]d ][ p<Yk<jQ][ <[G 1h<DQYQjs ]N +g]Og<ZZQ[O <[Ok<OIh <[G 0]]Yh ¥+ 01 ÃÁ¦ <j /+ / ÃÁÂÂ +]gjY<[G$gIO][1/!$Ej]DIgÃÁ Ê [XQE<<gQãQü6<hE]Z<g<Y!QOkIY]kY@]<[Ggk[]<gg]E<±-k<YQjsQ[1hI]N/ hkggI[jp<Yk<jQ][!IjP]Gh±[+g]EIIGQ[Oh]N jPI"$.1!°ÃÁÂÂ]QZDg<+]gjkO<Y/IdjIZDIgÃÁ ÂÁ [XQE<<gQãQü6<hE]Z<g<Y!QOkIY]kY@]<[Ggk[]<gg]E<±]qj]gI<EP<kh<DYI/ !]pQ[Oj]q<gG</shjIZ<jQEp<Yk<jQ][± [+g]EIIGQ[Oh ]N jPI ÆjP [jIg[<jQ][<Y 7]gXhP]d ][ !kYjQ+<g<GQOZ !]GIYQ[O ¥!+!°ÃÁ¦ <j !]GIYh ÃÁÂÂ 7IYYQ[Oj][ "Iq ;I<Y<[G //0]kg[<Y$Ej]DIgÃÁ $QNLFD%DULãLü  8VDELOLW\GULYHQGHYHORSPHQWZLWK86(0( 74 75 $XWRPDWHG$QDO\VLVRI7UDFHDELOLW\LQ &\EHU3K\VLFDO6\VWHPV )HUKDW(UDWD%HGLU7HNLQHUGRJDQ ,&±0XOWL3DUDGLJP 0RGHOOLQJ IRU &\EHU3K\VLFDO 6\VWHPV  &KDOOHQJHVRI7UDFHDELOLW\LQ,QGXVWU\ 6HPDQWLFDOO\PHDQLQJIXOWUDFHDELOLW\ WUDFHDELOLW\UHODWLRQVVKRXOGKDYHDULFKVHPDQWLFPHDQLQJ LQVWHDGRIEHLQJVLPSOHELGLUHFWLRQDOUHIHUHQWLDOUHODWLRQ &RQILJXUDELOLW\RIWUDFHDELOLW\SRVVLEO\G\QDPLFDOO\ WKH VHPDQWLFV RIWUDFHDELOLW\ LVRIWHQVWDWLFDOO\GHILQHG WKHVHPDQWLFVFDQQRWEHHDVLO\DGDSWHGIRUWKHQHHGVRI GLIIHUHQWSURMHFWV GLIIHUHQWWUDFHDEOHHOHPHQWVDQGWKHW\SHVRIUHODWLRQVH[LVWLQ LQGXVWULDOVHWWLQJV 6HYHUDOLQGXVWULHVGHPDQGVIRUPDOSURRIVRIWUDFHDELOLW\ &RQVLVWHQF\FKHFNLQJDQGUHSDLULQJEURNHQWUDFHOLQNV /ϭϰϬϰʹ DƵůƚŝͲWĂƌĂĚŝŐŵDŽĚĞůůŝŶŐĨŽƌLJďĞƌͲWŚLJƐŝĐĂů^LJƐƚĞŵƐ 76 :KDW LV WKHSUREOHP" ,QGXVWULDO8VH&DVHLQ$LUEXV 6\QFKURQL]DWLRQRIUHJXODWLRQGRFXPHQWDWLRQZLWKDGHVLJQ UXOHUHSRVLWRU\ 77  6,'36\VWHP,QVWDOODWLRQ'HVLJQ3ULQFLSOHV /ϭϰϬϰʹ DƵůƚŝͲWĂƌĂĚŝŐŵDŽĚĞůůŝŶŐĨŽƌLJďĞƌͲWŚLJƐŝĐĂů^LJƐƚĞŵƐ  &RPSRQHQW2QWRORJ\DQG5XOHV ^ƚƌƵĐƚƵƌĂůͺůĞŵĞŶƚ ƌĂĐŬĞƚ &ĂƐƚĞŶĞƌ WĐůĂŵƉ ƐƐĞŵďůLJ WŚLJƐŝĐĂů ĐŽŵƉŽŶĞŶƚ ůĂŵƉ WͲůĂŵƉ WͲůĂŵƉ E^ϱϱϭϲ ƚƚĂĐŚŵĞŶƚ ĚĞǀŝĐĞ ŽŵƉŽŶĞŶƚ ƐƐĞŵďůLJ KďũĞĐƚWƌŽƉĞƌƚŝĞƐ ƐƵďůĂƐƐKĨ ZĚĨƐůĂďĞů ^ŬŽƐƉƌĞĨ>ĂďĞů ŶŶŽƚĂƚŝŽŶWƌŽƉĞƌƚŝĞƐ WͲĐůĂŵƉE^ϱϱϭϲĐĂŶďĞĨŝdžĞĚŽŶyǁŝƚŚz WŚLJƐŝĐĂůĐŽŵƉŽŶĞŶƚ ^ƚĂŶĚĂƌĚƌĞĨĞƌĞŶĐĞ 2EMHFWLYHV DĂŶĂŐĞƌƵůĞƐĚĞƐŝŐŶƉƌŝŶĐŝƉůĞƐĂŶĚŝŵƉƌŽǀĞƚƌĂĐĞĂďŝůŝƚLJ ƵƚŽŵĂƚĞŝĚĞŶƚŝĨŝĐĂƚŝŽŶŽĨĚĞƐŝŐŶĐŽŶĨůŝĐƚƐĂŐĂŝŶƐƚƌƵůĞƐ 78 ,QGXVWULDO8VH&DVHLQ)RUG2WRVDQ 6\QFKURQL]DWLRQRI'HVLJQ6SHFLILFDWLRQVZLWK&RPSXWHU $LGHG'HVLJQ'DWDLQ3URGXFW/LIHF\FOH0DQDJHPHQW  %20DQG'HVLJQ6SHFLILFDWLRQV ŽŵƉƵƚĞƌͲĂŝĚĞĚĞƐŝŐŶĂƚĂ ŝůůŽĨDĂƚĞƌŝĂůĂƚĂ ĞƐŝŐŶZƵůĞƐ 79 ,QGXVWULDO8VH&DVHLQ+DYHOVDQ ,QWHJUDWLRQZLWK$SSOLFDWLRQ/LIHF\FOH0DQDJHPHQWWRHQVXUH UHOLDELOLW\DQGFRQVLVWHQF\LQWKHV\VWHPXQGHUGHYHORSPHQW 5HTXLUHPHQW &RQWUDFW 5HTXLUHPHQW 6\VWHP   7HVW &DVH 7HVWHG%\  7HVW 6WRU\%RDUG  'HVLJQ0RGHO  6WRU\%RDUG  5HTXLUHPHQW 6\VWHP   5HTXLUHPHQW 6RIWZDUH 3DUHQW &KLOG 5HTXLUHPHQW +DUGZDUH 3DUHQW  &KLHOG  7DVN 3DUHQW &KLOG %XJ &KDQJH 5HTXHVW   $FFHVVLEOH 2EMHFW  +\SHU/LQN  5HTXLUHPHQW &RQWUDFW 5HODWHG   5HODWHG   (QJLQHHULQJ &KDQJH 3URSRVDO $IIHFWHG%\  $IIHFW  7DVN 3DUHQW &KLOG 6KDUH3RLQW 'RFXPHQW  $WWDFKPHQW 3UHG  6XF  &RQILJXUDWLRQ ,WHP &RQWDLQV  $OORFDWHGWR  9DOLGDWLRQ 3ODQ 9DOLGDWHG%\  9DOLGDWHV  &KDQJHVHW ,PSOHPHQWHGE\ 7DUVNL$3ODWIRUPIRU$XWRPDWHG$QDO\VLVRI '\QDPLFDOO\&RQILJXUDEOH7UDFHDELOLW\ 6HPDQWLFV The Paper is accepted by “The 32nd ACM Symposium on Applied Computing (SAC’2017), Programming Languages Track”. 80  2YHUYLHZRI7HFKQLFDO&RQWULEXWLRQV #7DUVNL dĞĐŚŶŝĐĂů tŽƌŬƉĂĐŬĂŐĞƐ &ŽƌŵĂů ^ƉĞĐŝĨŝĐĂƚŝŽŶΘ &ŽƌŵĂů^ĞŵĂŶƚŝĐƐ dƌĂĐĞĂďŝůŝƚLJ DĂŶĂŐĞŵĞŶƚ dƌĂĐĞĂďŝůŝƚLJ sŝƐƵĂůŝnjĂƚŝŽŶ dƌĂĐĞĂďŝůŝƚLJĂƚĂͲ DŽĚĞů ƵƚŽŵĂƚĞĚ ŶĂůLJƐŝƐ ^ĞŵĂŶƚŝĐŽŵĂŝŶ ;dƌĂĐĞĂďŝůŝƚLJͿ >ŽĐĂƚŝŽŶƐ >ŝŶŬƐ ^LJŶƚĂdž ;&ŽƌŵĂůŝƐŵͿ &ŝƌƐƚͲŽƌĚĞƌ>ŽŐŝĐ džŝŽĂŵĂƚŝĐ^Ğƚ dŚĞŽƌLJ ZĞůĂƚŝŽŶĂů ĂůĐƵůƵƐ /ϭϰϬϰʹ DƵůƚŝͲWĂƌĂĚŝŐŵDŽĚĞůůŝŶŐĨŽƌLJďĞƌͲWŚLJƐŝĐĂů^LJƐƚĞŵƐ  $XWRPDWHG$QDO\VLVRI'\QDPLFDOO\ &RQILJXUHG7UDFHDELOLW\6HPDQWLFV dƌĂĐĞĂďŝůŝƚLJZƵůĞƐƚŽĚĞĨŝŶĞƚƌĂĐĞĂďŝůŝƚLJƐĞŵĂŶƚŝĐƐ sĂƌŝŽƵƐdƌĂĐĞĂďŝůŝƚLJŶĂůLJƐŝƐŵŝŐŚƚďĞƉĞƌĨŽƌŵĞĚ ƌƚĞĨĂĐƚƐŽƌƉĂƌƚŽĨĂƌƚĞĨĂĐƚƐ 81  7HFKQLFDO&RQWULEXWLRQV#7DUVNL &RQFHSWXDO0RGHOIRU7UDFHDELOLW\ /ϭϰϬϰʹ DƵůƚŝͲWĂƌĂĚŝŐŵDŽĚĞůůŝŶŐĨŽƌLJďĞƌͲWŚLJƐŝĐĂů^LJƐƚĞŵƐ  7HFKQLFDO&RQWULEXWLRQV#7DUVNL )RUPDOL]DWLRQRI7UDFHDELOLW\6HPDQWLFV /ϭϰϬϰʹ DƵůƚŝͲWĂƌĂĚŝŐŵDŽĚĞůůŝŶŐĨŽƌLJďĞƌͲWŚLJƐŝĐĂů^LJƐƚĞŵƐ 82  7DUVNL $SSURDFK /ϭϰϬϰʹ DƵůƚŝͲWĂƌĂĚŝŐŵDŽĚĞůůŝŶŐĨŽƌLJďĞƌͲWŚLJƐŝĐĂů^LJƐƚĞŵƐ  7HFKQLFDO&RQWULEXWLRQV#7DUVNL /ϭϰϬϰʹ DƵůƚŝͲWĂƌĂĚŝŐŵDŽĚĞůůŝŶŐĨŽƌLJďĞƌͲWŚLJƐŝĐĂů^LJƐƚĞŵƐ 83  7UDFHDELOLW\$QDO\VLV dƌĂĐĞĂďŝůŝƚLJ ŶĂůLJƐŝƐ ƵƚŽŵĂƚĞĚ ZĞĂƐŽŶŝŶŐ ŚĂŶŐĞ/ŵƉĂĐƚ ŶĂůLJƐŝƐ ŽŶƐŝƐƚĞŶĐLJ ĐŚĞĐŬŝŶŐ >ŽĐĂƚŝŽŶ ĚŝƐĐŽǀĞƌLJ ZĞĂƐŽŶŝŶŐŽŶ ƌĞůĂƚŝŽŶƐ ^ĐĂůĂďŝůŝƚLJ /ŶƚĞŐƌĂƚŝŽŶŽĨ ĨĨŝĐŝĞŶƚĞĐŝƐŝŽŶ WƌŽĐĞĚƵƌĞƐ /ŶĐƌĞŵĞŶƚĂů ƉƉƌŽĂĐŚ ƵƚŽŵĂƚĞĚ dƌĂĐĞďŝůŝƚLJ>ŝŶŬ ƌĞĂƚŝŽŶ ĞƚǁĞĞŶ DŽĚĞůŝŶŐ >ĂŶŐƵĂŐĞƐ DƵůƚŝͲ ŽŶƐŝƐƚĞŶĐLJ ŚĞĐŬŝŶŐ DŽĚĞů /ŶƚĞŐƌĂƚŝŽŶ dƌĂĐĞĂďŝůŝƚLJĂƚĂͲ DŽĚĞů /ϭϰϬϰʹ DƵůƚŝͲWĂƌĂĚŝŐŵDŽĚĞůůŝŶŐĨŽƌLJďĞƌͲWŚLJƐŝĐĂů^LJƐƚĞŵƐ  0RGHOLQJDQG5HDVRQLQJ$SSURDFKHV DŽĚĞůŝŶŐĂŶĚ ZĞĂƐŽŶŝŶŐ ŽŶƐƚƌĂŝŶƚ^ŽůǀŝŶŐ ;ŽƵŶĚĞĚDŽĚĞů ŚĞĐŬŝŶŐͿ <ŽĚ<ŽĚĂ ĐŽŶƐƚƌĂŝŶƚƐŽůǀĞƌ ĨŽƌƌĞůĂƚŝŽŶĂůůŽŐŝĐ ^d^ŽůǀĞƌƐ ůůŽLJŶĂůLJƐŝƐ ŶŐŝŶĞ <ŽĚ<ŽĚ dŚĞŽƌĞŵWƌŽǀĞƌƐ ϯŚŝŐŚ ƉĞƌĨŽƌŵĂŶĐĞ ƚŚĞƌŽŵƉƌŽǀĞƌ ^Dd^ŽůǀĞƌƐ DŽĚĞůŚĞĐŬŝŶŐ EƵyDsĂ ƐLJŵďŽůŝĐ ŵŽĚĞůĐŚĞĐŬĞƌ &ŝŶŝƚĞ^ƚĂƚĞ ^d^ŽůǀĞƌƐ /ŶĨŝŶŝƚĞ^ƚĂƚĞ ^Dd ^ŽůǀĞƌƐ ŽŶƐŝƐƚĞŶĐLJ ŚĞĐŬŝŶŐ ƌŽĐŽƉĂƚƚŽŽůĨŽƌ ĞĨĨŝĐŝĞŶƚƌĞůĂƚŝŽŶĂů ƉƌŽŐƌĂŵŵŝŶŐ ĨĨŝĐŝĞŶƚ'ƌĂƉŚ ůŐŽƌŝƚŚŵƐ <ŽĚ<ŽĚĂ ĐŽŶƐƚƌĂŝŶƚƐŽůǀĞƌ ĨŽƌƌĞůĂƚŝŽŶĂůůŽŐŝĐ džĂĐƚŽƵŶĚƐ &ŝƌƐƚͲŽƌĚĞƌ ƌĞůĂƚŝŽŶĂůůŽŐĐ dŚĞ^ĂƚŝƐĨŝĂďŝůŝƚLJ DŽĚƵůŽ dŚĞŽƌŝĞƐ >ŝďƌĂƌLJ ;^DdͲ>/Ϳ >ŝŶĞĂƌdĞŵƉŽƌĂů >ŽŐŝĐ;>d>Ϳ /ϭϰϬϰʹ DƵůƚŝͲWĂƌĂĚŝŐŵDŽĚĞůůŝŶŐĨŽƌLJďĞƌͲWŚLJƐŝĐĂů^LJƐƚĞŵƐ 90  7UDFHDELOLW\0DQDJHPHQW:3 dƌĂĐĞĂďŝůŝƚLJ DĂŶĂŐĞŵĞŶƚ ĐůŝƉƐĞsŝĞǁƐ dƌĂĐĞĂďŝůŝƚLJsŝĞǁ ŽŶƚĞdžƚƵĂůsŝĞǁ dĂƌŐĞƚŵĂƉƉŝŶŐ ^ŽƵƌĐĞŵĂƉƉŝŶŐ ĐůŝƉƐĞtŝnjĂƌĚƐ DĂƌŬǁƚLJƉĞ ĞůĞƚĞDĂƌŬ DĂƉDĂƌŬĞƌ ZĞŵŽǀĞ ŚĂŶŐĞdLJƉĞ ĐůŝƉƐĞĐƚŝŽŶƐ ,LJƉĞƌůŝŶŬ ĚĞƚĞĐƚŽƌƐĂŶĚ ŵĞŶƵ ƌĂŐĂŶĚƌŽƉ ^ƵƉƉŽƌƚĞĚ ĐůŝƉƐĞĚŝƚŽƌƐ EĂǀŝŐĂƚŝŽŶ /ϭϰϬϰʹ DƵůƚŝͲWĂƌĂĚŝŐŵDŽĚĞůůŝŶŐĨŽƌLJďĞƌͲWŚLJƐŝĐĂů^LJƐƚĞŵƐ  'HPRQVWUDWLRQ 7UDFHDELOLW\0DQDJHPHQWLQ$FWLRQ /ϭϰϬϰʹ DƵůƚŝͲWĂƌĂĚŝŐŵDŽĚĞůůŝŶŐĨŽƌLJďĞƌͲWŚLJƐŝĐĂů^LJƐƚĞŵƐ 91  'LVFXVVLRQ )LUVWRUGHUWKHRU\RIUHODWLRQVWREHDVROXWLRQIRUWUDFHDELOLW\LQ 030&36"  3UHOLPLQDU\UHVXOWVVKRZVWKDWWKHDSSURDFKZRUNVRQWKH V\QFKURQL]DWLRQRIGHVLJQUXOHVZLWKGHVLJQLQVWDOODWLRQRISK\VLFDO FRPSRQHQWV &XUUHQWO\'3//7VROYHUGRHVQRWH[LVWVIRUWKHWKHRU\ :KDWDERXWRWKHUWKHRULHVDQGFRPELQDWLRQRIWKHRULHV" 6KRXOGZHFRQVLGHUDOVRWKHWHPSRUDOEHKDYLRURIWKH WUDFHDELOLW\" /ϭϰϬϰʹ DƵůƚŝͲWĂƌĂĚŝŐŵDŽĚĞůůŝŶŐĨŽƌLJďĞƌͲWŚLJƐŝĐĂů^LJƐƚĞŵƐ 7KDQN\RXIRU\RXUDWWHQWLRQ :HYDOXH\RXURSLQLRQDQG TXHVWLRQV 92 A hybrid master (discrete-event and discretetime) for Functional Mockup Interface Vincent Albert LAAS-CNRS / University of Toulouse MPM4CPS workshop – Malaga, Spain, 2016 COST Action IC1404 Overview Introduction Solution Experiments Conclusion and perspectives 2 93 Introduction 3 Discrete-time simulation ௗ௫ሺ௧ሻ ௗ௧ ൌ݂ݔݐǡݑݐ ݔ௜ݐ൅݄ൌݔ௜ݐ൅ௗ௫೔ሺ௧ሻ ௗ௧ Ǥ݄ 4 94 Discrete-event simulation  ሶݍݐൌ݂ݍݐǡݑݐ ݍݐ൅ȟݐൌݍݐ൅ሶݍݐǤȟݐ ȟൌݍݐ൅ȟݐെݍሺݐሻ 5 Discrete-event simulation  ሶݍݐൌ݂ݍݐǡݑݐ ݍݐ൅ȟݐൌݍݐ൅ሶݍݐǤȟݐ ȟൌݍݐ൅ȟݐെݍሺݐሻ 1. The required time for the solution of ݍݐ to change by ȟis οݐൌቐ୼୕ሶ௤݂݅ ሶݍ്Ͳ λ݋ݐ݄݁ݎݓ݅ݏ݁ At this time, the next state will be ݍݐ௞൅οݐൌݍݐ௞൅ݏ݅݃݊ ሶݍݐ௞כοܳ 6 95 Discrete-event simulation  ሶݍݐൌ݂ݍݐǡݑݐ ݍݐ൅ȟݐൌݍݐ൅ሶݍݐǤȟݐ ȟൌݍݐ൅ȟݐെݍሺݐሻ 1. The required time for the solution of ݍݐ to change by ȟis οݐൌቐ୼୕ሶ௤݂݅ ሶݍ്Ͳ λ݋ݐ݄݁ݎݓ݅ݏ݁ At this time, the next state will be ݍݐ௞൅οݐൌݍݐ௞൅ݏ݅݃݊ ሶݍݐ௞כοܳ 2. If ሶݍchanges of value before ݐ௞൅οݐthen ݍൌݍ൅ሶݍכ݁ οݐൌ ൞ οܳെݍെݍ݈ ሶݍ ݂݅ ሶݍ്Ͳ λ݋ݐ݄݁ݎݓ݅ݏ݁ 7 Discrete-Event System Specification ൏ܺǡܻǡܵǡߜ݅݊ݐǡߜ݁ݔݐǡߜܿ݋݊ǡɉǡݐܽ൐ ݐܽ׷ܵ՜Թ଴ǡஶ ା Model DEVS Atomic component Simulator DEVS Parallel DEVS protocol 8 96 Issues h<0 is false at the integration step before ݐଵ h<0 is true at the integration step aݐଵ DEVS FMU 3. Get time of FMU next event 2. Handle FMU input external event 9 1. Continuous /discrete interface 4. Handle FMU internal event Hybrid Master for DEVS-FMI 10 97 DEVS-FMI for ME 11 double predictState(double t) { currentTime = t; horizon = t + lookAheadHorizon; while (currentTime < horizon) currentTime = integrate(currentTime+lookAheadStepSize); newState = fmi2getContinuousState(); outputs = fmi2getReal(); predictions.add(newState); eventInds = fmi2GetEventIndicators() for(eventInds.size) if(eventInds[i] != savedeventInds[i]) handleEvent(); //bisectional search return currentTime; return currentTime; } Experiments 12 98 BouncingBall 13 DC-Motor and PWM Controller 14 99 Quantities Model-Based Representation Domain Model Example Instance: ܮ݁݊݃ݐ݄ ͳͲ േ ͲǤͲͲͳ ݉ 11 8QLW QDPH6WULQJ V\PERO6WULQJ GLPHQVLRQV5HDO>@ FRQYHUVLRQ)DFWRU5HDO>@ RIIVHW5HDO>@ 85HDO [5HDO X 5HDO 4XDQWLW\ YDOXH XQLW P8QLW QDPH 0HWHU V\PERO P GLPHQVLRQV ! FRQYHUVLRQ)DFWRU ! RIIVHW ! XU85HDO [  X  T4XDQWLW\ YDOXH XQLW Example 12 0HDVXUH WLPH4XDQWLW\ SRVLWLRQ4XDQWLW\ VWDUW 6HFWLRQ0HDVXUH GXUDWLRQ4XDQWLW\ GLVWDQFH4XDQWLW\ DYJ9HORFLW\4XDQWLW\ DYJ$FFHOHUDWLRQ4XDQWLW\ HQG duration = end.time – start.time distance = end.position – start.position avgVelocity = distance / duration avgAcceleration = (end.velocity – start.velocity) / duration YHORFLW\ 4XDQWLW\ Start A B C N… Measure M0 M1 M2 M3 MN S1 S2 S3 106 Unit Operations 13 8QLW LV%DVH8QLW%RROHDQ LV'HULYHG8QLW%RROHDQ LV8QLWOHVV%RROHDQ LV'LPHQVLRQOHVV%RROHDQ LV&RPSDWLEOH:LWK8QLWX%RROHDQ HTXDOV8QLWX%RROHDQ PXOWLSO\8QLWV8QLWX8QLW GLYLGH8QLWV8QLWX8QLW SRZHU8QLWV5HDOV8QLW Query nature of unit Combine units Compare units Measurement Uncertainty Operations 14 85HDO DGGU85HDO85HDO PLQXVU85HDO85HDO PXOWLSO\U85HDO85HDO GLYLGH%\U85HDO85HDO SRZHUV5HDO85HDO « OHVV7KDQU85HDO%RROHDQ OHVV7KDQ2U(TXDOVU85HDO%RROHDQ JUHDWHU7KDQU85HDO%RROHDQ « Arithmetic operations Comparison operations 107 Quantity Operations 15 4XDQWLW\ FRPSDWLEOH8QLWVT4XDQWLW\%RROHDQ FRQYHUW7RX8QLW4XDQWLW\ FRQYHUW7R6,8QLWV4XDQWLW\ « DGGT4XDQWLW\4XDQWLW\ PLQXVT4XDQWLW\ 4XDQWLW\ PXOWLSO\T4XDQWLW\ 4XDQWLW\ GLYLGH%\T4XDQWLW\ 4XDQWLW\ « OHVV7KDQT4XDQWLW\%RROHDQ OHVV7KDQ2U(TXDOVT4XDQWLW\%RROHDQ JUHDWHU7KDQT4XDQWLW\%RROHDQ « Arithmetic operations Comparison operations Unit conversion operations Unit comparison Example 16 VWDUW 66HFWLRQ0HDVXUH GXUDWLRQ    V GLVWDQFH   P DYJ9HORFLW\    PV DYJ$FFHOHUDWLRQ    PVð HQG duration = end.time – start.time distance = end.position – start.position avgVelocity = distance / duration avgAcceleration = (end.velocity – start.velocity) / duration 00HDVXUH WLPH V SRVLWLRQ P YHORFLW\ PV 00HDVXUH WLPH   V SRVLWLRQ P YHORFLW\ PV Start A B C N… Measure M0 M1 M2 M3 MN S1 S2 S3 108 Available Implementations Java: Reference implementation OCL (USE Tool): Specification of operations with preconditions and postconditions Support for imperative use of operations (SOIL) UML (Papyrus, MagicDraw): Support for specifying quantities and computations with quantities Proof-of-concept prototype for executing computations with quantities with fUML Download: https://github.com/moliz/moliz.quantitytypes Implementation 17 USE Tool: https://sourceforge.net/projects/useocl/ MagicDraw: http://www.nomagic.com/products/magicdraw.html Eclipse Papyrus UML: https://eclipse.org/papyrus/ Java Example Length initialPosition = new Length(0, 0.001, Units.Meter); Length finalPosition = new Length(10, 0.001, Units.Meter); Length distance = finalPosition.minus(initialPosition); USE OCL Example !new UReal(’ip’) !ip.x : = 0.0 !ip.u := 0.001 !new Quantity(’initialPosition’) !initialPosition.value := ip ... !distance := finalPosition.minus(initialPosition) Papyrus UML Example Ongoing and Future Work Implementation Evolve fUML proof-of-concept implementation to full implementation Alf implementation (textual action language for fUML) Full integration with Papyrus and MagicDraw Eclipse OCL implementation Refinement of the conceptual model of quantity types Different kinds of uncertainty (e.g., interval, different probability distributions) Different kinds of units (e.g., length units, time units, etc.) Representation of quantities Useable representation of quantities Integration with existing standards, e.g., MARTE and SysML 18 109 Thank You! Questions? Manuel Wimmer [email protected] Antonio Vallecillo [email protected] Tanja Mayerhofer [email protected] Contact Loli Burgueño [email protected] A. Vallecillo, C. Morcillo, and P. Orue. Expressing Measurement Uncertainty in Software Models. In Proc. of 10th Int. Conf. on the Quality of Information and Communications Technology (QUATIC), 1–10, 2016. T. Mayerhofer, M. Wimmer, A. Vallecillo. Adding Uncertainty and Units to Quantity Types in Software Models. In Proc. of 2016 ACM SIGPLAN Int. Conf. on Software Language Engineering (SLE), ACM, 118–131, 2016. References 110 INTEGRATING UNCERTAINTY MODELLING WITH USE CASE MODELLING TO DISCOVER UNKNOWNS Tao Yue, ShaukatAli and Man Zhang (tao, shaukat, manzhang}@simula.no http://www.zen-tools.com http://www.u-test.eu/ Chief Research Scientist, Simula Research Laboratory, Oslo, Norway T T T Y Y S S S h h h k k k Workshop of ICT COST Action1404, Malaga, 2016 U-Test is a EU-funded H2020 project (2015 Jan. – 2017 Dec.) 2 TESTING CYBER-PHYSICAL SYSTEMS UNDER UNCERTAINTY Website: http://www.u-test.eu Overall Funding: 3.71 Million Euros Duration: 2015 to 2018 # Partners: 9 We are going beyond the scope of this project and establishing a long-term, industry-oriented research foundation towards this direction. 111 Two industrial CPS 3 Automated Warehouse (AW) ULMA Handling Systems, Spain Geo Sports (GS) Future Position X (FPX), Sweden http://www.u-test.eu/use-cases/ U-Model U-RUCM Uncertainty Modeling Framework U-Evolve U-Testing U-RUCM is an extension to RUCM for specifying uncertaintiesas part of system requirements. Conceptual model RUCM (Req. Spe.) Test Ready Models in UML Class Diagrams and State Machines 112 The U-Model takes a subjective approach to represent uncertainty. BeliefModel MeasureModel <<import>> Uncertainty Model U <<import>> Man Zhang, Bran Selic, Shaukat Ali, Tao Yue, Oscar Okariz and Roland Norgren, Understanding Uncertainty in CyberPhysical Systems: A Conceptual Model, 12th European Conference on Modelling Foundations and Applications (ECMFA), 2016. https://www.simula.no/file/u-modeltrfinalpdf/download U-MODEL – BELIEF MODEL 6 Measure 1 = objective concept = subjective concept BeliefAgent Belief 1..* Belief Statement 0..* substatements Evidence 0..* «enumeration» IndeterminacyNature nondeterminism insufficientResolution missingInfo composite unclassified Indeterminacy Source source 0..* /source1..* 0..* Uncertainty 0..* 0..* 0..* 0..* Measurement 113 The Uncertainty Model Expands On Uncertainty From Several Different Viewpoints And Introduces Related Abstractions. 7 Uncertainty Geographical Location Occurrence Content Time Environment Pattern 0..* Lifetime 0..1 Locality 0..1 «ISO 3000» Risk 0..1 Effect 0..1 0..* dependency The Purpose Of The Measure Model Is To Give A High-level Introduction Of Commonly Known Uncertainty Measures . 8 Measure Probability Ambiguity Vagueness Fuzziness NonSpecificity 114 U-RUCM integrates U-Model and RUCM. 9 Belief Template Is Newly Introduced To Specify Belief Use Case Specification, Which Inherits The RUCM Template. 101 0 Key Heading Fields Different Flow of Events 115 We apply the best strategy to test the real case study in terms of discovering uncertainties. 9 Test Case Generation Test Case Minimization Test Case Execution GeoSports APML 336 98 #TC #Min. TC %Min. Observed Uncertainty 2085 83.9% Unique Uncertainties 18 New Uncertainty Test infrastructures have been built, which enable the introduction of known indeterminacy sources . -Signal Shielding box and Far From Locator - Unknown indeterminacy sources Acknowledgement 10 122 References  Man Zhang, Bran Selic, Shaukat Ali, Tao Yue, Oscar Okariz and Roland Norgren, Understanding Uncertainty in Cyber-Physical Systems: A Conceptual Model, 12th European Conference on Modelling Foundations and Applications (ECMFA), 2016. https://www.simula.no/file/u-modeltrfinalpdf/download  Man Zhang, Tao Yue, Shaukat Ali, Bran Selic, Oscar Okariz, Roland Norgren, Karmele Intxausti, Santiago Charramendieta. Specifying Uncertainty in Use Case Models in Industrial Settings. Simula Research Laboratory, Technical Report 2016. https://www.simula.no/publications/specifying-uncertainty-use-case-models-industrial-settings  Man Zhang, Shaukat Ali, Tao Yue and Malin Hedman. Uncertainty-based Test Case Generation and Minimization for CyberPhysical Systems: A Multi-Objective Search-based Approach. Simula Research Laboratory, 2016. https://www.simula.no/publications/uncertainty-based-test-case-generation-and-minimization-cyber-physical-systems-multi  Tao Yue, Shaukat Ali, Bran Selic, Uncertainty Modeling, Request for Information, Object Management Group, 2016, http://www.omg.org/members/cgi-bin/doc?ad/16-08-01.pdf  Tao Yue, Shaukat Ali, Man Zhang and Dipesh Pradhan. Standardization Bodies and Standards Relevant for Uncertainty Modelling, Simula Research Laboratory, Technical Report 2016-05, 2016.https://www.simula.no/publications/standardizationbodies-and-standards-relevant-uncertainty-modelling  Man Zhang, Shaukat Ali, Tao Yue and Roland Norgren, Interactively Evolving Test Ready Models with Uncertainty Developed for Testing Cyber-Physical Systems, Submitted to a Journal, https://www.simula.no/file/ist-u-evolvesubmittedtrpdf/download  Man Zhang, Shaukat Ali, Tao Yue and Roland Norgren. An Integrated Modeling Framework to Facilitate Model-Based Testing of Cyber-Physical Systems under Uncertainty, Submitted to a Journal, Simula Research Laboratory, Technical Report 2016-02, 2016.https://www.simula.no/file/sosympaperfinaltrpdf/download 11 123 Separation of Concerns in Continuous Time Hierarchical Co-simulation Cl´audio Gomes, Joachim Denil, Bart Meyers, Hans Vangheluwe IC1404 – Multi-Paradigm Modelling for Cyber-Physical Systems November 24–25, 2016, Malaga, Spain Motivation Simulation has helped us so far. . . . . . but not to its full potential. Complex systems have to be partitioned into sub-systems, developed by specialized teams. Their own M&S tools; Some are external companies; Leading to locally (but not globally) optimal solutions: Models of each partial solution cannot be integrated; IP cannot be cheaply disclosed; 124 Co-simulation Theory and techniques to enable global simulation of a coupled system, via the composition of sub-system simulators. Sub-system simulators are virtual mock-ups: Executable binaries; Common API for communication. . . . . . but many different capabilities! I/ O Coup li ng: I/O Coupling Co-simulator: Co-sim Scenario Solver Model + Inputs Outputs Orchestration Algorithm (BUS) Co-simulator Inputs Outputs Simulator Time-stepped communication; Continuous-time dynamics; Approximated inputs; Physical laws; Instantaneous reactions; Solver Model + Inputs Outputs Simulator Si=Xi,Ui,Yi,δ i,λ i,xi(0),φ Ui δi:R×Xi×Ui→Xi λi:R×Xi×Ui→Yior R×Xi→Yi xi(0) ∈Xi φUi:R×Ui×...×Ui→Ui Inputs State O utputs extrapolation co-sim step micro-step 125 Co-simulation Scenario CS =UCS ,YCS ,{Si},L,φ UCS  L:Y1×...×Yn×YCS ×U1×...×Un×UCS →Rm ALGORITHM 1: Orchestration. Data: An autonomous scenario CS =∅,YCS ,{Si},L,∅ and a communication step size H. Result: A co-simulation trace. t:= 0; while true do Solve: yi(t)=λi(t,xi(t),ui(t)),for i=1,...,n L(y1(t),...,yn(t),yCS (t),u1(t),...,un(t)) = ¯ 0; xi(t+H):=δi(t,xi(t),ui(t)),for i=1,...,n; t:= t+H; end CS =∅,∅,{S1,S2},L,∅ L=⎡ ⎣ uk−x1 v1 u1−Fk ⎤ ⎦ Concerns Limited Communication: Computer A Computer B Causality Conflict: ...... Algebraic Loops: Strongly Coupled Clusters: Requires: Availability Requires: Jacobian Requires: I/O Dependency 126 Example: Strongly Coupled Clusters Scenario ˙ x1 v1=F1(x1 v1,u1) λ1=x1 v1 ˙ x2 v2=F2(x2 v2,uk uc) λ2=Fk Fc ˙ x3 v3=F3(x3 v3,u3) λ3=x3 v3 Example: Strongly Coupled Clusters Sensitivity ˙ x1 v1=F1(x1 v1,u1) ˙ x2 v2=F2(x2 v2,uk uc) ˙ x3 v3=F3(x3 v3,u3) ∂F1 ∂u1 is small ∂F2 ∂uk is small ∂F2 ∂uc is Large ∂F3 ∂u3 is Large m1=1 c1=0.1 d1=0.5 m2=1 ck=0.1dk=0.1 cc=2 dc=1.3 m3=1 c3=0.1 d3=0.1 127 Example: Strongly Coupled Clusters Sensitivity Strongly Coupled Clusters Optimization Step: Step: Step: 128 Strongly Coupled Clusters Results H=0.01 max x1−˜x1=0.0294 max x2−˜x2=0.0583 max x3−˜x3=0.0582 H=0.1 H=0.005 max x1−˜x1=0.0340 max x2−˜x2=0.0217 max x3−˜x3=0.0214 Conclusion Our approach, underpinned by MDD: Introduce artificial simulators to solve local concerns; Optimize conflicting concerns at global level; Correctness verified via: Analytical solutions with toy examples; Simulation of the coupled model; High accuracy co-simulation; Benefits: Leverage existing standards for co-simulation; Systematically address concerns while reusing existing orchestration algorithms; Downsides (Future work): Keep scenarios readable; Huge search space for conflicting concerns; Lack of formal proof of convergence; 129 Thank you! Bibliography [1] Torsten Blockwitz, Martin Otter, Johan Akesson, Martin Arnold, Christoph Clauss, Hilding Elmqvist, Markus Friedrich, Andreas Junghanns, Jakob Mauss, Dietmar Neumerkel, Hans Olsson, and Antoine Viel. Functional Mockup Interface 2.0: The Standard for Tool independent Exchange of Simulation Models. In 9th International MODELICA Conference, pages 173–184, Munich, Germany, nov 2012. Link¨ oping University Electronic Press; Link¨ opings universitet. [2] Cl´audio Gomes. Foundations for Co-simulation – IWT Proposal. Technical report, University of Antwerp, Antwerp, 2015. [3] Cl´audio Gomes. Foundations for Continuous Time Hierarchical Co-simulation. In ACM Student Research Competition (ACM/IEEE 19th International Conference on Model Driven Engineering Languages and Systems),pagetoappear,Saint Malo,Brittany,France,2016. [4] Bert Van Acker, Joachim Denil, Paul De Meulenaere, Hans Vangheluwe, Bert Vanacker, and Paul Demeulenaere. Generation of an Optimised Master Algorithm for FMI Co-simulation. In Proceedings of the Symposium on Theory of Modeling & Simulation-DEVS Integrative, pages 946–953. Society for Computer Simulation International, 2015. [5] K Vanherpen, J Denil, P De Meulenaere, and H Vangheluwe. Design-Space Exploration in Model Driven Engineering: An Initial Pattern Catalogue. In Proceedings of the First International Workshop on Combining Modelling with Searchand Example-Based Approaches (CMSEBA), co-located with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), pages 42–51. CEUR Workshop Proceedings (Vol-1340), sep 2014. 130 ,&± 0XOWL3DUDGLJP0RGHOOLQJIRU&\EHU3K\VLFDO6\VWHPV 0RGHOLQJRI&RRSHUDWLRQ%HKDYLRULQ IOH[LEOH 9HKLFOH 3ODWRRQ EDVHG RQ + \EULG $ XWRPDWRQ 9HKLFOH  3ODWRRQ EDVHG  RQ  + \EULG  $ XWRPDWRQ DQG3UHGLFLWLYH$QDO\VLV >ĞũůĂ ĂŶũĂŶŽǀŝĐͲDĞŚŵĞĚŽǀŝĐ &ĂĐƵůƚLJŽĨůĞĐƚƌŝĐĂůŶŐŝŶĞĞƌŝŶŐhŶŝǀĞƌƐŝƚLJŽĨdƵnjůĂ ŽƐŶŝĂĂŶĚ,ĞƌnjĞŐŽǀŝŶĂ K^d/ϭϰϬϰ EŽǀĞŵďĞƌϮϰͲϮϱϮϬϭϲ DĂůĂŐĂ^ƉĂŝŶ ϭ &RQWHVW ŽŽƉĞƌĂƚŝǀĞŝŶƚĞůůŝŐĞŶƚƚƌĂŶƐƉŽƌƚƐLJƐƚĞŵ;Ͳ/d^Ϳ ,LJďƌŝĚĂƵƚŽŵĂƚŽŶŵŽĚĞůŝŶŐŽĨĨůĞdžŝďůĞsĞŚŝĐůĞ WůĂƚŽŽŶ  dƌĂĨĨŝĐ ĂƚĂ ŶĂůLJƚŝĐ WƌĞĚŝĐƚŝŽŶ ŽĨ ĐŽŽƉĞƌĂƚŝǀĞ  dƌĂĨĨŝĐ  ĂƚĂ  ŶĂůLJƚŝĐ  WƌĞĚŝĐƚŝŽŶ  ŽĨ  ĐŽŽƉĞƌĂƚŝǀĞ  ďĞŚĂǀŝŽƌƉƌŽĨŝůĞƵƐŝŶŐŶĞƵƌĂůŶĞƚǁŽƌŬĂŶĚĨƵnjnjLJʹ ŶĞƵƌŽ;E&/^Ϳ K^d/ϭϰϬϰ EŽǀĞŵďĞƌϮϰͲϮϱϮϬϭϲDĂůĂŐĂ^ƉĂŝŶ Ϯ 131 7UDIILFLQIRUPDWLRQSUHGLFWLRQV dƌĂĨĨŝĐŝŶĨŽƌŵĂƚŝŽŶƉƌĞĚŝĐƚŝŽŶƐ ƐƉĞĞĚ ĨůŽǁĂŶĚ ƚƌĂǀĞůƚŝŵĞ dŚ ƚ ŝ Ĩ ŝ ƚŝ ƚ ĨĨŝ Ĩů Ěŝ ƚŝ Ś  dŚ ƌĞĞĐĂ ƚ ĞŐŽƌ ŝ ĞƐŽ Ĩ Ğdž ŝ Ɛ ƚŝ ŶŐ ƚ ƌĂ ĨĨŝ Đ Ĩů ŽǁƉƌĞ Ěŝ Đ ƚŝ ŽŶĂƉƉƌŽĂĐ Ś ĞƐ ĂƌĞƌĞĐŽŐŶŝnjĞĚ ƚŝŵĞͲƐĞƌŝĞƐĂƉƉƌŽĂĐŚĞƐ;ZDĂŶĚZ/DŵŽĚĞůͿ ƉƌŽďĂďŝůŝƐƚŝĐĂƉƉƌŽĂĐŚĞƐ;ĂLJĞƐŝĂŶŶĞƚǁŽƌŬDĂƌŬŽǀĐŚĂŝŶ ĂŶĚDĂƌŬŽǀƌĂŶĚŽŵĨŝĞůĚƐͿĂŶĚ ŶŽŶƉĂƌĂŵĞƚƌŝĐĂƉƉƌŽĂĐŚĞƐ;ĂƌƚŝĨŝĐŝĂůŶĞƵƌĂůŶĞƚǁŽƌŬƐ ƐƵƉƉŽƌƚǀĞĐƚŽƌƌĞŐƌĞƐƐŝŽŶ;^sZͿƚŚĞĂĚĂƉƚŝǀĞŶĞƵƌŽͲĨƵnjnjLJ ƐLJƐƚĞŵ;E&/^ͿͿ K^d/ϭϰϬϰ EŽǀĞŵďĞƌϮϰͲϮϱϮϬϭϲDĂůĂŐĂ^ƉĂŝŶ ϭϱ $GDSWLYH1HXUUR)X]]\$1),6 SUHGLFWLRQPHWKRG dŚĞĂƌƚŝĨŝĐŝĂůŶĞƵƌĂůŶĞƚǁŽƌŬ;EEͿͲ ĂƐĂŶĂŶĂůLJƚŝĐĂůŵĞƚŚŽĚĨŽƌ ǀĂƌŝŽƵƐƉƌĞĚŝĐƚŝŽŶ ƉƵƌƉŽƐĞƐĞŶĞĨŝƚŝŶĚĞƉĞŶĚĞŶĐLJŽŶƚŚĞ ŬŶŽǁůĞĚŐĞŽĨŝŶƚĞƌŶĂůƐLJƐƚĞŵƉĂƌĂŵĞƚĞƌƐ ĐŽŵƉƌĞƐƐĞĚĐŽŵƉĂĐƚ ƐŽůƵƚŝŽŶŝŶƚĞƌŵƐŽĨŵƵůƚŝͲǀĂƌŝĂďůĞƉƌŽďůĞŵƐĂŶĚƌĂƉŝĚ ĐŽŵƉƵƚĂƚŝŽŶ K^d/ϭϰϬϰ EŽǀĞŵďĞƌϮϰͲϮϱϮϬϭϲDĂůĂŐĂ ^ƉĂŝŶ ĐŽŵƉƵƚĂƚŝŽŶ  dŚĞE&/^ŝƐĂ ƉĂƌƚŝĐƵůĂƌĐůĂƐƐŽĨƚŚĞEEĨĂŵŝůLJǁŝƚŚĂƚƚƌĂĐƚŝǀĞ ĞƐƚŝŵĂƚŝŽŶĂŶĚůĞĂƌŶŝŶŐƉŽƚĞŶƚŝĂůƐ dŚĞE&/^ĐŽŵďŝŶĞƐƚŚĞƉŽǁĞƌŽĨƚŚĞ&/^ǁŝƚŚĂŶĞƵƌĂůŶĞƚǁŽƌŬ ďĂĐŬͲƉƌŽƉĂŐĂƚŝŽŶůĞĂƌŶŝŶŐĂůŐŽƌŝƚŚŵ ĚĂƉƚŝǀĞŶĞƵƌŽͲĨƵnjnjLJ;E&/^ͿĐŽŵƉƵƚŝŶŐƚĞĐŚŶŝƋƵĞͲ ƚŽĞƐƚŝŵĂƚĞ ƚŚĞĐŽŽƉĞƌĂƚŝǀĞŝŶƚĞƌĂĐƚŝŽŶƐƉƌŽĨŝůĞŝŶƌĞůĂƚŝŽŶƚŽƚŚĞƐƉĞĞĚƐŽĨ ƚŚĞůĞĂĚĞƌĂŶĚĨŝƌƐƚĂŶĚƐĞĐŽŶĚĨŽůůŽǁĞƌǀĞŚŝĐůĞƐ ϭϲ 138 1HXUUR)X]]\0RGHO$1),6 dŚĞE&/^ƐƚƌƵĐƚƵƌĞĐŽŶƐŝƐƚƐŽĨϱůĂLJĞƌƐ ƉƌĞŵŝƐĞƉĂƌĂŵĞƚĞƌƐ K^d/ϭϰϬϰ EŽǀĞŵďĞƌϮϰͲϮϱϮϬϭϲDĂůĂŐĂ ^ƉĂŝŶ ŵĞŵďĞƌƐŚŝƉůĂLJĞƌ ƌƵůĞůĂLJĞƌ ĐŽŶƐĞƋƵĞŶƚƉĂƌĂŵĞƚĞƌƐ ŽƵƚƉƵƚůĂLJĞƌ $1),6 VWUXFWXUH ϭϳ 3UHGLFWLRQUHVXOWVRIFRRSHUDWLRQ EHKDYLRU SURILOH XVLQJ$1),6 ZD^;ƌŽŽƚŵĞĂŶ ƐƋƵĂƌĞĞƌƌŽƌͿ ĐŽĞĨĨŝĐŝĞŶƚŽĨ ĚĞƚĞƌŵŝŶĂƚŝŽŶ;ZϮͿ dŚ ď ů Ĩ K^d/ϭϰϬϰ EŽǀĞŵďĞƌϮϰͲϮϱϮϬϭϲDĂůĂŐĂ ^ƉĂŝŶ  dŚ Ğ ď ĞƐƚƌĞƐƵ ů ƚŽ Ĩ  ƉƌĞĚŝĐƚŝŽŶZϮсϬϵϵ ZD^сϬϭϱϱĂŶĚ D^сϬϬϮĨŽƌϳ'ĂƵƐƐ ŵĞŵďĞƌƐŚŝƉĨƵŶĐƚŝŽŶƐ ĨŽƌĞĂĐŚŝŶƉƵƚ ǀĂƌŝĂďůĞƐŝŶϭϬĞƉŽĐŚƐ ϭϴ / %DQMDQRYLF0HKPHGRYLF 1 'HOLF , %XWLJDQ 6 .DVDSRYLF DQG , %RVDQNLF 1HXURIX]]\ SUHGLFWLRQ RI FRRSHUDWLRQ LQWHUDFWLRQ SURILOH RI IOH[LEOH URDG WUDLQ EDVHG RQ K\EULG DXWRPDWRQ PRGHOLQJ WK ,QWHUQDWLRQDO &RQIHUHQFH RQ 7UDQVSRUWDWLRQ DQG 7UDIILF (QJLQHHULQJ ,&77(  SS  /XFHUQ 6ZLW]HUODQG  139 1HXUDOQHWZRUNDVSUHGLFWLRQPHWKRG dŚĞĂƌƚŝĨŝĐŝĂůŶĞƵƌĂůŶĞƚǁŽƌŬ;EEͿͲ ĂƐĂŶĂŶĂůLJƚŝĐĂůŵĞƚŚŽĚĨŽƌ ǀĂƌŝŽƵƐƉƌĞĚŝĐƚŝŽŶ ƉƵƌƉŽƐĞƐ ĞŶĞĨŝƚŝŶĚĞƉĞŶĚĞŶĐLJŽŶƚŚĞŬŶŽǁůĞĚŐĞŽĨŝŶƚĞƌŶĂůƐLJƐƚĞŵ ƉĂƌĂŵĞƚĞƌƐ ĐŽŵƉƌĞƐƐĞĚĐŽŵƉĂĐƚƐŽůƵƚŝŽŶŝŶƚĞƌŵƐŽĨŵƵůƚŝͲ ŝďů ďů Ě ŝĚ ŝ K^d/ϭϰϬϰ EŽǀĞŵďĞƌϮϰͲϮϱϮϬϭϲDĂůĂŐĂ^ƉĂŝŶ ǀĂƌ ŝ Ă ďů ĞƉƌŽ ďů ĞŵƐĂŶ Ě ƌĂƉ ŝĚ ĐŽŵƉƵƚĂƚ ŝ ŽŶ EZyŶĞƵƌĂůŶĞƚǁŽƌŬͲ ƚŽĞƐƚŝŵĂƚĞƚŚĞĐŽŽƉĞƌĂƚŝǀĞŝŶƚĞƌĂĐƚŝŽŶƐ ƉƌŽĨŝůĞŝŶƌĞůĂƚŝŽŶƚŽƚŚĞƐƉĞĞĚƐŽĨƚŚĞůĞĂĚĞƌĂŶĚĨŝƌƐƚĂŶĚƐĞĐŽŶĚ ĨŽůůŽǁĞƌǀĞŚŝĐůĞƐ ϭϵ 6WUXFWXUHRI1$5; EZyŶĞƵƌĂůŶĞƚǁŽƌŬͲ ĨĞĞĚďĂĐŬ ĚLJŶĂŵŝĐŶĞƵƌĂůŶĞƚǁŽƌŬƚŚĞ ŽƵƚƉƵƚƐŝŶƚŝŵĞƐĞƌŝĞƐĚĞƉĞŶĚƐ ŽĨĐƵƌƌĞŶƚŝŶƉƵƚƐĂŶĚƉƌĞǀŝŽƵƐ ŽƵƚƉƵƚƐ dŚĞŝŶƉƵƚƉĂƌĂŵĞƚĞƌƐ ŽĨƚŚĞ EZyŶĞƚǁŽƌŬ Ͳ ƚŚĞƚŝŵĞƐĞƌŝĞƐ ŽĨƚŚĞůĞĂĚĞƌĨŝƌƐƚĂŶĚƐĞĐŽŶĚ ĨŽůůŽǁĞƌƐƐƉĞĞĚƐ dŚĞŽƵƚƉƵƚƉĂƌĂŵĞƚĞƌŽĨƚŚĞ EZyŶĞƚǁŽƌŬ Ͳ ƚŚĞƌŽĂĚ ĐŽŽƉĞƌĂƚŝŽŶďĞŚĂǀŝŽƵƌƉƌŽĨŝůĞ ĨƌŽŵƚŚĞWůĂƚŽŽŶŚLJďƌŝĚ ĂƵƚŽŵĂƚŽŶ K^d/ϭϰϬϰ EŽǀĞŵďĞƌϮϰͲϮϱϮϬϭϲDĂůĂŐĂ^ƉĂŝŶ ϮϬ 140 3UHGLFWLRQUHVXOWVRIFRRSHUDWLRQ EHKDYLRU SURILOH XVLQJ1$5; K^d/ϭϰϬϰ EŽǀĞŵďĞƌϮϰͲϮϱϮϬϭϲDĂůĂŐĂ^ƉĂŝŶ Ϯϭ 3UHGLFWLRQUHVXOWVRIFRRSHUDWLRQ EHKDYLRU SURILOH XVLQJ1$5;IRUFDVH QRLVHGWHVWGDWD K^d/ϭϰϬϰ EŽǀĞŵďĞƌϮϰͲϮϱϮϬϭϲDĂůĂŐĂ^ƉĂŝŶ ϮϮ ĞŚĂǀŝŽƵƌ ƐĐĞŶĂƌŝŽǁŝƚŚϯϮϬϭƐĂŵƉůĞƐ /%DQMDQRYLF0HKPHGRYLF,%XWLJDQ0.DQWDUG]LF6.DVDSRYLF3UHGLFWLRQRI&RRSHUDWLYH3ODWRRQLQJ 0DQHXYHUV XVLQJ1$5;1HXUDO1HWZRUN,(((6PDUWV\VWHPVDQG7HFKQRORJ\667 SS &URDWLD2FWREDU 141 &RQFOXVLRQ &ůĞdžŝďůĞsĞŚŝĐůĞWůĂƚŽŽŶ ŚLJďƌŝĚĂƵƚŽŵĂƚŽŶŵŽĚĞůͲ ĚĞǀĞůŽƉĞĚƚŽƐŝŵƵůĂƚĞĐŽŶƚƌŽůĂŶĚĐŽŽƉĞƌĂƚŝŽŶŝŶƚĞƌĂĐƚŝŽŶƐ ďĞƚǁĞĞŶƚŚĞǀĞŚŝĐůĞƐ ;ũŽŝŶŵĞƌŐĞůĞĂǀĞ WůĂƚŽŽŶͿ dŚĞƉƌŽƉŽƐĞĚŽƵƚƉƵƚďĞŚĂǀŝŽƌĨƵŶĐƚŝŽŶ ĨƌŽŵ ďĞŚĂǀŝŽƵƌƉĂƚƚĞƌŶƐŽĨ ƚŚĞZŽĂĚdƌĂŝŶ ƚŽ ƐƉĞĐŝĨŝĐ ĐŽŽƉĞƌĂƚŝŽŶďĞŚĂǀŝŽƌ ƉƌŽĨŝůĞ Ͳ ĚĞƐĐƌŝďĞƐ ƚŚĞĐŽŵƉůĞdž ƐLJƐƚĞŵŝŶƚĞƌĂĐƚŝŽŶƐŽŶůLJǁŝƚŚŽŶĞǀĂƌŝĂďůĞ dŚĞEZyEĞƵƌĂůŶĞƚǁŽƌŬĂŶĚE&/^ƚĞĐŚŶŝƋƵĞŚĂǀĞ ďĞĞŶ ƵƐĞĚĨŽƌƉƌĞĚŝĐƚŝŽŶŽĨĨůĞdžŝďůĞsĞŚŝĐůĞWůĂƚŽŽŶĐŽŽƉĞƌĂƚŝŽŶ ďĞŚĂǀŝŽƌ WƌŽĨŝůĞƵƐĞĨƵůĨŽƌ/ŶƚĞůůŝŐĞŶƚdƌĂĨĨŝĐDĞŶĂŐĞŵĞŶƚƐLJƐƚĞŵ ƉƌĞĚŝĐƚŝŽŶŽĨƚƌĂĨĨŝĐŵŽďŝůŝƚLJŝŶ/d^ĂƐƐŽĐŝĂƚĞĚǁŝƚŚ ƵŶĐĞƌƚĂŝŶƚŝĞƐ K^d/ϭϰϬϰ EŽǀĞŵďĞƌϮϰͲϮϱϮϬϭϲDĂůĂŐĂ ^ƉĂŝŶ Ϯϯ 142 Introduction to Physical-Systems Modelling with Bond Graphs Jan F. Broenink University of Twente, NL 24 November, Malaga, Spain C1404 – Multi-Paradigm Modelling for Cyber-Physical Systems Tutorial-BG.key - 24 November 2016 Jan Broenink young MPM4CPS, 17+18+ (19) Dec 2015 @ UT Modelling — basics •System •Parts forming a whole; parts have functional relationship •Has boundary: what belongs to the system and what not •Model (of a system) •Description of a system: parts & relations •SimpliRed, but complex enough -to study phenomena relevant for our problem context •Competent Model -as simple as possible, but sufRcient for the goal of the model •Modelling goals -understand dynamic behaviour -compute a reaction in a control system -predict in a design context 2 Figures taken from: J van Amerongen “Dynamical Systems” text book, see reference on slide 31 Sometimes referred to as Fig n.n JvA Tutorial-BG.key - 24 November 2016 143 Jan Broenink young MPM4CPS, 17+18+ (19) Dec 2015 @ UT Modelling - choices what eects to describe •Network of basic elements •complex: structure in submodels, sub-submodels etc •What to model •depends on purpose / goal •Our case •understand physics / dynamic behaviour -on a rather global level -a network of elements •control law design -function blocks (transfer functions) is enough 3 Tutorial-BG.key - 24 November 2016 Jan Broenink young MPM4CPS, 17+18+ (19) Dec 2015 @ UT Interaction in Models •Unilateral •signals approach •Bilateral •physical-systems approach •mutual inSuence •exchange of energy 4 Fig 1.4 and 1.5 JvA Tutorial-BG.key - 24 November 2016 144 Jan Broenink young MPM4CPS, 17+18+ (19) Dec 2015 @ UT Modeling: essential dynamics •Dynamics •Behaviour depends on the past! •Change of variables is essential here •Time •continuous value of time •observe at Rxed intervals: discrete time •Examples 5 Tutorial-BG.key - 24 November 2016 Jan Broenink CPS - PSMC / ECSI 3A/B, 201500053 Modelling: physics domains, bond graphs •Domains •Electro-Magnetic, Mechanical: translation, rotation •Hydraulic, Thermal •Physical effects •in all domains the same •resulting in the same equations! •9 basic elements •C, I, R, Se, Sf •TF: transformer; GY: gyrator •Network: -common effort => 0 junction -common Sow => 1 junction 6    , &  5 06H Tutorial-BG.key - 24 November 2016 145 Jan Broenink young MPM4CPS, 17+18+ (19) Dec 2015 @ UT Ideal behaviour — real components •Ideal: only the essential effect (only one) •Elementary behaviour •Components •physical thing… Spring = spring, and mass, and friction, and? •parasitic effects •Lumped-parameter Models •assume all elementary properties concentrated in elements -mass => point mass -spring => only the spring behaviour, nothing more 7 Tutorial-BG.key - 24 November 2016 Jan Broenink CPS - PSMC / ECSI 3A/B, 201500053 Electrical Domain •Physics Concepts •Ideal Physical Models •Transformer •like ideal electrical transformer -u 1 = n u 2 -i 2 = n i 1 -n = n 1 / n 2 •Gyrator •artiRcial element when within domain -u 1 = r i 2 -u 2 = r i 1 8               transformer Capacitor Resistor inductance TF, GY: only transduce! P 1 = P 2 Tutorial-BG.key - 24 November 2016 146 Jan Broenink CPS - PSMC / ECSI 3A/B, 201500053 Mechanical Domain •Physics Concepts •Ideal Physical Models •Transformer •like ideal lever / gears / chain wheels -F 1 = n F 2 -v 2 = n v 1 -n = n 1 / n 2 •Gyrator •transduction in electromotor -u 1 = r  2 -T 2 = r i 1 9 transformers TF, GY: only transduce! P 1 = P 2                see later! Tutorial-BG.key - 24 November 2016 Jan Broenink young MPM4CPS, 17+18+ (19) Dec 2015 @ UT Bond Graphs — Essence •Essential Idea •Graph to describe dynamic behaviour •Exchange of energy (Sow of power between nodes) -Domain-independent •Graphs: Bond Graphs / Ideal Physical Models •Directed graph: submodels & ideal connections •5 basic physical effects -storage (C, I), dissipation (R), transformation (TF, GY), networks (0, 1), sources (Se, Sf) •Model elements -describe only one single physical effect -compound structures: network of elements •Encapsulation of contents •Interface: ports with 2 variables -(u, i): voltage & current; (F, v): force & velocity •Equations as equalities (math. Equations) -Not as algorithm: u = i * R -> u := i * R of i := u / R 10 Tutorial-BG.key - 24 November 2016 147