

FOLLOWUS
RISE, School of Computer and Information Science, Southwest University, Chongqing 400715, China
Beijing Institute of Control Engineering, Beijing 100190, China
School of Computer Science, Northwestern Polytechnical University, Xi'an 710029, China
College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, China
[ "Bo LIU, E-mail: iubocq@swu.edu.cn" ]
Bin GU, gubinbj@sina.com
Tie-xin WANG, tiexin.wang@nuaa.edu.cn
Received:29 June 2020,
Revised:2020-10-22,
Published:2020-11
Scan QR Code
LIU Bo, ZHANG Yuan-rui, CAO Xue-lian, et al. A survey of model-driven techniques and tools for cyber-physical systems[J]. Frontiers of Information Technology & Electronic Engineering, 2020, 21(11): 1567-1590.
LIU Bo, ZHANG Yuan-rui, CAO Xue-lian, et al. A survey of model-driven techniques and tools for cyber-physical systems[J]. Frontiers of Information Technology & Electronic Engineering, 2020, 21(11): 1567-1590. DOI: 10.1631/FITEE.2000311.
信息物理融合系统(cyber-physical system,CPS)已成为应对社会经济可持续发展诸多挑战性问题的潜在使能技术。自2006年CPS肇始至今的大量研究表明:CPS由大量异构子系统构成,其系统构建是一个困难且复杂的工程。在既有的CPS构建实践中,较之其他复杂系统设计方法,模型驱动方法展现出显著优势。鉴于此,本文针对CPS的模型驱动开发方法展开综述:介绍当前模型驱动开发中广泛使用的方法、技术与工具,并讨论其在CPS构建中的应用;同时,从建模语言、功能及应对CPS构建挑战性问题的能力等方面,对比分析这些技术与工具。基于这些工作,本文认为:尽管模型驱动方法尚需持续改进其理论、技术与工具,但其仍不失为构建CPS的必由之路;此外,可支持不同建模方法的统一建模平台已是迫切需求,统一平台不仅有利于学术研究及工业实践活动,也利于提升工业界与学术界的协作。
Cyber-physical systems (CPSs) have emerged as a potential enabling technology to handle the challenges in social and economic sustainable development. Since it was proposed in 2006
intensive research has been conducted
showing that the construction of a CPS is a hard and complex engineering process due to the nature of integrating a large number of heterogeneous subsystems. Among other approaches to dealing with the complex design issues
model-driven design of CPSs has shown its advantages. In this review paper
we present a survey of research on model-driven development of CPSs. We are concerned mainly with the widely used methods
techniques
and tools
and discuss how these are applied to CPSs. We also present comparative analyses on the surveyed techniques and tools from various perspectives
including their modeling languages
functionalities
and the challenges which they address in CPS design. With our understanding of the surveyed methods
we believe that model-driven approaches are an inevitable choice in building CPSs and further research effort is needed in the development of model-driven theories
techniques
and tools. We also argue that a unified modeling platform is needed. Such a platform would benefit research in the academic community and practical development in industry
and improve the collaboration between these two communities.
JR Abrial . . The B-Book: Assigning Programs to Meanings . . Cambridge University Press, Cambridge, UK , , 2005 . . .
JR Abrial , , , M Butler , , , S Hallerstede , , , 等 . . Rodin: an open toolset for modelling and reasoning in Event-B . . Int J Softw Tools Technol Transfer , , 2010 . . 12 ( ( 6 ): ): 447 - - 466 . . DOI: 10.1007/s10009-010-0145-y http://doi.org/10.1007/s10009-010-0145-y . .
M Amrani , , , L Lucio , , , G Selim , , , 等 . . A tridimensional approach for studying the formal verification of model transformations . . Proc IEEE $5^{\rm th}$ Int Conf on Software Testing, Verification and Validation , , 2012 . . p.921 - - 928 . . DOI: 10.1109/ICST.2012.197 http://doi.org/10.1109/ICST.2012.197 . .
R Banach , , , M Butler , , , SC Qin , , , 等 . . Core Hybrid Event-B I: single Hybrid Event-B machines . . Sci Comput Program , , 2015 . . 105 92 - - 123 . . DOI: 10.1016/j.scico.2015.02.003 http://doi.org/10.1016/j.scico.2015.02.003 . .
R Banach , , , M Butler , , , SC Qin , , , 等 . . Core Hybrid Event-B II: multiple cooperating Hybrid Event-B machines . . Sci Comput Program , , 2017 . . 139 1 - - 35 . . DOI: 10.1016/j.scico.2016.12.003 http://doi.org/10.1016/j.scico.2016.12.003 . .
A Banerjee , , , S Kandula , , , T Mukherjee , , , 等 . . BAND-AiDe: a tool for cyber-physical oriented analysis and design of body area networks and devices . . ACM Trans Embed Comput Syst , , 2012 . . 11 ( ( S2 ): ): 49 DOI: 10.1145/2331147.2331159 http://doi.org/10.1145/2331147.2331159 . .
C Bernardeschi , , , A Domenici , , , P Masci . . A PVS-Simulink integrated environment for model-based analysis of cyber-physical systems . . IEEE Trans Softw Eng , , 2018 . . 44 ( ( 6 ): ): 512 - - 533 . . DOI: 10.1109/TSE.2017.2694423 http://doi.org/10.1109/TSE.2017.2694423 . .
P Bocciarelli , , , A D'Ambrogio , , , A Giglio , , , 等 . . A BPMN extension for modeling cyber-physical-production-systems in the context of Industry 4.0 . . IEEE $14^{\rm th}$ Int Conf on Networking, Sensing and Control , , 2017 . . p.599 - - 604 . . DOI: 10.1109/ICNSC.2017.8000159 http://doi.org/10.1109/ICNSC.2017.8000159 . .
G Booch , , , J Rumbaugh , , , I Jacobson . . The Unified Modeling Language User Guide . . Addison Wesley Longman Publishing Co., Inc., USA , , 1999 . . .
A Boronat , , , JA Carsí , , , I Ramos . . Exogenous model merging by means of model management operators . . Proc $3^\rm{rd}$ Workshop on Software Evolution Through Transformations: Embracing the Change , , 2006 . . p.1 - - 19 . . DOI: 10.14279/tuj.eceasst.3.8 http://doi.org/10.14279/tuj.eceasst.3.8 . .
G Brau , , , N Navet , , , J Hugues . . Heterogeneous models and analyses in the design of real-time embedded systems—an avionic case-study . . Proc $25^{\rm th}$ Int Conf on Real-Time Networks and Systems , , 2017 . . p.168 - - 177 . . DOI: 10.1145/3139258.3139281 http://doi.org/10.1145/3139258.3139281 . .
W Braun , , , F Casella , , , B Bachmann . . Solving large-scale Modelica models: new approaches and experimental results using OpenModelica . . Proc $12^{\rm th}$ Int Modelica Conf , , 2017 . . p.557 - - 563 . . DOI: 10.3384/ecp17132557 http://doi.org/10.3384/ecp17132557 . .
D Broman , , , EA Lee , , , S Tripakis , , , 等 . . Viewpoints, formalisms, languages, and tools for cyber-physical systems . . Proc $6^{\rm th}$ Int Workshop on Multi-paradigm Modeling , , 2012 . . p.49 - - 54 . . DOI: 10.1145/2508443.2508452 http://doi.org/10.1145/2508443.2508452 . .
AW Brown . . Model driven architecture: principles and practice . . Softw Syst Model , , 2004 . . 3 ( ( 4 ): ): 314 - - 327 . . DOI: 10.1007/s10270-004-0061-2 http://doi.org/10.1007/s10270-004-0061-2 . .
M Broy , , , MV Cengarle , , , E Geisberger . . Cyber-physical systems: imminent challenges.In: Calinescu R, Garlan D (Eds.), Large-Scale Complex IT Systems. Development, Operation and Management . . Springer, Berlin , , 2012 . . p.1 - - 28 . . DOI: 10.1007/978-3-642-34059-8_1 http://doi.org/10.1007/978-3-642-34059-8_1 . .
J Cabot , , , M Gogolla . . Object Constraint Language (OCL): a definitive guide . . Proc $12^{\rm th}$ Int Conf on Formal Methods for the Design of Computer, Communication, and Software Systems: Formal Methods for Model-Driven Engineering , , 2012 . . p.58 - - 90 . . DOI: 10.1007/978-3-642-30982-3_3 http://doi.org/10.1007/978-3-642-30982-3_3 . .
D Calegari , , , N Szasz . . Verification of model transformations: a survey of the state-of-the-art . . Electron Notes Theor Comput Sci , , 2013 . . 292 5 - - 25 . . DOI: 10.1016/j.entcs.2013.02.002 http://doi.org/10.1016/j.entcs.2013.02.002 . .
LP Chen , , , MA Babar , , , B Nuseibeh . . Characterizing architecturally significant requirements . . IEEE Softw , , 2013 . . 30 ( ( 2 ): ): 38 - - 45 . . DOI: 10.1109/MS.2012.174 http://doi.org/10.1109/MS.2012.174 . .
X Chen , , , ZM Liu . . Towards interface-driven design of evolving component-based architectures. In: Hinchey M, Bowen JP, Olderog ER (Eds.), Provably Correct Systems . . Springer, Cham , , 2017 . . p.121 - - 148 . . DOI: 10.1007/978-3-319-48628-4_6 http://doi.org/10.1007/978-3-319-48628-4_6 . .
A Cicchetti , , , D di Ruscio , , , R Eramo , , , 等 . . JTL: a bidirectional and change propagating transformation language . . Proc $3^{\rm rd}$ Int Conf on Software Language Engineering , , 2010 . . p.183 - - 202 . . DOI: 10.1007/978-3-642-19440-5_11 http://doi.org/10.1007/978-3-642-19440-5_11 . .
EM Clarke . . The birth of model checking. In: Grumberg O, Veith H (Eds.), 25 Years of Model Checking: History, Achievements, Perspectives . . Springer, Berlin , , 2008 . . p.1 - - 26 . . DOI: 10.1007/978-3-540-69850-0_1 http://doi.org/10.1007/978-3-540-69850-0_1 . .
K Czarnecki , , , S Helsen . . Classification of model transformation approaches . . Proc $2^{{\rm nd}}$ OOPSLA Workshop on Generative Techniques in the Context of the Model Driven Architecture , , 2003 . . p.1 - - 17 . . . .
P Derler , , , EA Lee , , , AS Vincentelli . . Modeling cyber-physical systems . . Proc IEEE , , 2012 . . 100 ( ( 1 ): ): 13 - - 28 . . DOI: 10.1109/JPROC.2011.2160929 http://doi.org/10.1109/JPROC.2011.2160929 . .
JC Eidson , , , EA Lee , , , S Matic , , , 等 . . Distributed real-time software for cyber-physical systems . . Proc IEEE , , 2012 . . 100 ( ( 1 ): ): 45 - - 59 . . DOI: 10.1109/JPROC.2011.2161237 http://doi.org/10.1109/JPROC.2011.2161237 . .
ESTEREL . . Efficient development of safe avionics software with DO-178C objectives using SCADE Suite Ⓡ . . ESTEREL Technologies , , 2015 . . 2020 http://www.peraglobal.com/upload/contents/2015/11/20151113142739_85462.pdf http://www.peraglobal.com/upload/contents/2015/11/20151113142739_85462.pdf , , [Accessed on Aug. 30, 2020] . .
PH Feiler , , , DP Gluch , , , JJ Hudak . . The Architecture Analysis $\& $ Design Language (AADL): an introduction . . Software Engineering Institute , , 2006 . . p.145 DOI: 10.1184/R1/6584909 http://doi.org/10.1184/R1/6584909 . .
M Fowler . . UML Distilled: a Brief Guide to the Standard Object Modeling Language ($3^{\rm rd}$ Ed.) . . Addison-Wesley, Boston, USA , , 2003 . . .
S Friedenthal , , , A Moore , , , R Steiner . . A Practical Guide to SysML: the Systems Modeling Language . . Elsevier, Waltham, USA , , 2015 . . .
P Fritzson . . Principles of Object Oriented Modeling and Simulation with Modelica 3.3: a Cyber-Physical Approach . . John Wiley & Sons, Inc , , 2014 . . DOI: 10.1002/9781118989166 http://doi.org/10.1002/9781118989166 . .
N Fulton , , , S Mitsch , , , JD Quesel , , , 等 . . KeYmaera X: an axiomatic tactical theorem prover for hybrid systems . . Proc $25^{\rm th}$ Int Conf on Automated Deduction , , 2015 . . p.527 - - 538 . . DOI: 10.1007/978-3-319-21401-6_36 http://doi.org/10.1007/978-3-319-21401-6_36 . .
H Gill . . From Vision to Reality: Cyber-Physical Systems , , 2008 . . 2020 http://labs.ece.uw.edu/nsl/aar-cps/Gill_HCSS_Transportation_Cyber-Physical_Systems_2008.pdf http://labs.ece.uw.edu/nsl/aar-cps/Gill_HCSS_Transportation_Cyber-Physical_Systems_2008.pdf , , [Accessed on Aug. 30, 2020] . .
V Gunes , , , S Peter , , , T Givargis , , , 等 . . A survey on concepts, applications, and challenges in cyber-physical systems . . KSII Trans Int Inform Syst , , 2014 . . 8 ( ( 12 ): ): 4242 - - 4268 . . DOI: 10.3837/tiis.2014.12.001 http://doi.org/10.3837/tiis.2014.12.001 . .
N Halbwachs , , , P Caspi , , , P Raymond , , , 等 . . The synchronous data flow programming language LUSTRE . . Proc IEEE , , 1991 . . 79 ( ( 9 ): ): 1305 - - 1320 . . DOI: 10.1109/5.97300 http://doi.org/10.1109/5.97300 . .
JF He , , , Q Li . . A hybrid relational modelling language.In: Gibson-Robinson T, Hopcroft P, Lazić R (Eds.), Concurrency, Security, and Puzzles: Essays Dedicated to Andrew William Roscoe on the Occasion of His $60^{\rm th}$ Birthday . . Springer, Cham , , 2017 . . p.124 - - 143 . . DOI: 10.1007/978-3-319-51046-0_7 http://doi.org/10.1007/978-3-319-51046-0_7 . .
P Hehenberger , , , B Vogel-Heuser , , , D Bradley , , , 等 . . Design, modelling, simulation and integration of cyber physical systems: methods and applications . . Comput Ind , , 2016 . . 82 273 - - 289 . . DOI: 10.1016/j.compind.2016.05.006 http://doi.org/10.1016/j.compind.2016.05.006 . .
D Henriksson , , , H Elmqvist . . Cyber-physical systems modeling and simulation with Modelica . . Proc $8^{\rm th}$ Int Modelica Conf , , 2011 . . p.502 - - 509 . . DOI: 10.3384/ecp11063502 http://doi.org/10.3384/ecp11063502 . .
TA Henzinger . . The theory of hybrid automata . . Proc $11^{\rm th}$ Annual IEEE Symp on Logic in Computer Science , , 1996 . . p.278 - - 292 . . DOI: 10.1109/LICS.1996.561342 http://doi.org/10.1109/LICS.1996.561342 . .
P Huang , , , KQ Jiang , , , CL Guan , , , 等 . . Towards modeling cyber-physical systems with SysML/MARTE/ pCCSL . . IEEE $42^{\rm nd}$ Annual Computer Software and Applications Conf , , 2018 . . p.264 - - 269 . . DOI: 10.1109/COMPSAC.2018.00042 http://doi.org/10.1109/COMPSAC.2018.00042 . .
JM Jézéquel , , , O Barais , , , F Fleurey . . Model driven language engineering with Kermeta . . Proc $3^{\rm rd}$ Int Summer School Conf on Generative and Transformational Techniques in Software Engineering III , , 2009 . . p.201 - - 221 . . DOI: 10.1007/978-3-642-18023-1_5 http://doi.org/10.1007/978-3-642-18023-1_5 . .
V Jirkovský , , , M Obitko , , , V Mařík . . Understanding data heterogeneity in the context of cyber-physical systems integration . . IEEE Trans Ind Inform , , 2017 . . 13 ( ( 2 ): ): 660 - - 667 . . DOI: 10.1109/TII.2016.2596101 http://doi.org/10.1109/TII.2016.2596101 . .
F Jouault , , , J Bézivin . . KM3: a DSL for metamodel specification . . Proc $8^{\rm th}$ IFIP WG 6.1 Int Conf on Formal Methods for Open Object-Based Distributed Systems , , 2006 . . p.171 - - 185 . . DOI: 10.1007/11768869_14 http://doi.org/10.1007/11768869_14 . .
F Jouault , , , F Allilaire , , , J Bézivin , , , 等 . . ATL: a model transformation tool . . Sci Comput Program , , 2008 . . 72 ( ( 1-2 ): ): 31 - - 39 . . DOI: 10.1016/j.scico.2007.08.002 http://doi.org/10.1016/j.scico.2007.08.002 . .
MB Juric , , , B Mathew , , , P Sarang . . Business Process Execution Language for Web Services: BPEL and BPEL4WS . . Packt Publishing , , 2004 . . .
A Kleppe , , , J Warmer , , , W Bast . . MDA Explained: the Model Driven Architecture: Practice and Promise . . Addison-Wesley, Boston , , 2003 . . .
T Kühne . . Matters of (meta-) modeling . . Softw Syst Model , , 2006 . . 5 ( ( 4 ): ): 369 - - 385 . . . .
BR Larson , , , P Chalin , , , J Hatcliff . . BLESS: formal specification and verification of behaviors for embedded systems with software . . Proc $5^{\rm th}$ Int Symp on NASA Formal Methods , , 2013 . . p.276 - - 290 . . DOI: 10.1007/978-3-642-38088-4_19 http://doi.org/10.1007/978-3-642-38088-4_19 . .
G Lasnier , , , J Cardoso , , , P Siron , , , 等 . . Distributed simulation of heterogeneous and real-time systems . . Proc IEEE/ACM $17^{\rm th}$ Int Symp on Distributed Simulation and Real Time Applications , , 2013 . . p.55 - - 62 . . DOI: 10.1109/DS-RT.2013.14 http://doi.org/10.1109/DS-RT.2013.14 . .
M Lawley , , , J Steel . . Practical declarative model transformation with Tefkat . . MoDELS Int Workshops Doctoral Symp , , 2005 . . p.139 - - 150 . . DOI: 10.1007/11663430_15 http://doi.org/10.1007/11663430_15 . .
EA Lee . . Cyber physical systems: design challenges . . Int Symp on Object/Component/Service-Oriented Real-Time Distributed Computing , , 2008 . . http://chess.eecs.berkeley.edu/pubs/427.html http://chess.eecs.berkeley.edu/pubs/427.html , , . .
EA Lee . . CPS foundations . . Proc $47^{\rm th}$ Design Automation Conf , , 2010 . . p.737 - - 742 . . http://chess.eecs.berkeley.edu/pubs/804.html http://chess.eecs.berkeley.edu/pubs/804.html , , . .
EA Lee . . Modeling in engineering and science . . Commun ACM , , 2018 . . 62 ( ( 1 ): ): 35 - - 36 . . DOI: 10.1145/3231590 http://doi.org/10.1145/3231590 . .
EA Lee , , , HY Zheng . . Operational semantics of hybrid systems . . Proc $8^{\rm th}$ Int Workshop on Hybrid Systems: Computation and Control , , 2005 . . p.25 - - 53 . . DOI: 10.1007/978-3-540-31954-2_2 http://doi.org/10.1007/978-3-540-31954-2_2 . .
EA Lee , , , M Niknami , , , TS Nouidui , , , 等 . . Modeling and simulating cyber-physical systems using CyPhySim . . Proc $20^{\rm th}$ Int Conf on Embedded Software , , 2015 . . p.115 - - 124 . . . .
J Lee , , , B Bagheri , , , HA Kao . . A cyber-physical systems architecture for Industry 4.0-based manufacturing systems . . Manuf Lett , , 2015 . . 3 18 - - 23 . . DOI: 10.1016/j.mfglet.2014.12.001 http://doi.org/10.1016/j.mfglet.2014.12.001 . .
KRM Leino . . Verification of Object-Oriented Software. The KeY Approach . . Springer, Berlin , , 2007 . . .
J Liu , , , JD Lv , , , Z Quan , , , 等 . . A calculus for hybrid CSP . . Proc $8^{\rm th}$ Asian Symp on Programming Languages and Systems , , 2010 . . p.1 - - 15 . . DOI: 10.1007/978-3-642-17164-2_1 http://doi.org/10.1007/978-3-642-17164-2_1 . .
J Liu , , , TF Li , , , ZH Ding , , , 等 . . AADL+: a simulation-based methodology for cyber-physical systems . . Front Comput Sci , , 2019 . . 13 ( ( 3 ): ): 516 - - 538 . . DOI: 10.1007/s11704-018-7039-7 http://doi.org/10.1007/s11704-018-7039-7 . .
Y Liu , , , Y Peng , , , BL Wang , , , 等 . . Review on cyber-physical systems . . IEEE/CAA J Autom Sin , , 2017 . . 4 ( ( 1 ): ): 27 - - 40 . . DOI: 10.1109/JAS.2017.7510349 http://doi.org/10.1109/JAS.2017.7510349 . .
ZM Liu , , , X Chen . . Model-driven design of object and component systems . . Engineering Trustworthy Software Systems, Cham , , 2016 . . p.152 - - 255 . . . .
ZM Liu , , , JP Bowen , , , B Liu , , , 等 . . Software abstractions and human-cyber-physical systems architecture modelling . . $5^{\rm th}$ Int School on Engineering Trustworthy Software Systems , , 2019 . . p.159 - - 219 . . DOI: 10.1007/978-3-030-55089-9_5 http://doi.org/10.1007/978-3-030-55089-9_5 . .
S Lunel , , , S Mitsch , , , B Boyer , , , 等 . . Parallel composition and modular verification of computer controlled systems in differential dynamic logic. In: Ter Beek M, McIver A, Oliveira J (Eds.), Formal Methods—The Next 30 Years . . Springer, Cham , , 2019 . . p.354 - - 370 . . DOI: 10.1007/978-3-030-30942-8_22 http://doi.org/10.1007/978-3-030-30942-8_22 . .
N Lynch , , , R Segala , , , F Vaandrager . . Hybrid I/O automata . . Inform Comput , , 2003 . . 185 ( ( 1 ): ): 105 - - 157 . . DOI: 10.1016/S0890-5401(03)00067-1 http://doi.org/10.1016/S0890-5401(03)00067-1 . .
O Maler , , , Z Manna , , , A Pnueli . . From timed to hybrid systems . . In: de Bakker JW, Huizing C, de Roever WP, et al. (Eds.), Real-Time: Theory in Practice. Springer, Berlin , , 1992 . . p.447 - - 484 . . DOI: 10.1007/BFb0032003 http://doi.org/10.1007/BFb0032003 . .
F Mallet . . MARTE/CCSL for modeling cyber-physical systems. In: Drechsler R, Kühne U (Eds.), Formal Modeling and Verification of Cyber-Physical Systems . . Springer Vieweg, Wiesbaden , , 2015 . . p.26 - - 49 . . DOI: 10.1007/978-3-658-09994-7_2 http://doi.org/10.1007/978-3-658-09994-7_2 . .
F Mallet , , , E Villar , , , F Herrera . . MARTE for CPS and CPSoS: present and future, methodology and tools. In: Nakajima S, Talpin JP, Toyoshima M, et al. (Eds.), Cyber-Physical System Design from an Architecture Analysis Viewpoint . . Springer, Singapore , , 2017 . . p.81 - - 108 . . DOI: 10.1007/978-981-10-4436-6_4 http://doi.org/10.1007/978-981-10-4436-6_4 . .
SJ Mellor . . MDA Distilled: Principles of Model-Driven Architecture . . Addison-Wesley, Boston , , 2004 . . 2020 http://cds.cern.ch/record/1505924 http://cds.cern.ch/record/1505924 , , [Accessed on Aug. 30, 2020] . .
T Mens , , , P van Gorp . . A taxonomy of model transformation . . Electron Notes Theor Comput Sci , , 2006 . . 152 125 - - 142 . . DOI: 10.1016/j.entcs.2005.10.021 http://doi.org/10.1016/j.entcs.2005.10.021 . .
J Miller , , , J Mukerji . . MDA Guide Version 1.0.1 . . Object Management Group , , 2003 . . .
MA Mohamed , , , M Challenger , , , G Kardas . . Applications of model-driven engineering in cyber-physical systems: a systematic mapping study . . J Comput Lang , , 2020 . . 59 100972 DOI: 10.1016/j.cola.2020.100972 http://doi.org/10.1016/j.cola.2020.100972 . .
A Müller , , , S Mitsch , , , W Retschitzegger , , , 等 . . A component-based approach to hybrid systems safety verification. In: Ábrahám E, Huisman M (Eds.), Integrated Formal Methods . . Springer, Cham , , 2016 . . p.441 - - 456 . . DOI: 10.1007/978-3-319-33693-0_28 http://doi.org/10.1007/978-3-319-33693-0_28 . .
S Nazari , , , C Sonntag , , , S Engell . . A Modelica-based modeling and simulation framework for large-scale cyber-physical systems of systems . . IFAC-PapersOnLine , , 2015 . . 48 ( ( 1 ): ): 920 - - 921 . . DOI: 10.1016/j.ifacol.2015.05.190 http://doi.org/10.1016/j.ifacol.2015.05.190 . .
J Oldevik , , , T Neple , , , R Grønmo , , , 等 . . Toward standardised model to text transformations . . Proc $1^{\rm st}$ European Conf on Model Driven Architecture: Foundations and Applications , , 2005 . . p.239 - - 253 . . DOI: 10.1007/11581741_18 http://doi.org/10.1007/11581741_18 . .
A Platzer . . Differential dynamic logic for hybrid systems . . J Autom Reason , , 2008 . . 41 ( ( 2 ): ): 143 - - 189 . . DOI: 10.1007/s10817-008-9103-8 http://doi.org/10.1007/s10817-008-9103-8 . .
A Platzer . . Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics . . Springer, Berlin , , 2010 . . .
A Platzer . . Logical Foundations of Cyber-Physical Systems . . Springer, Cham , , 2018 . . .
C Ptolemaeus . . System Design, Modeling, and Simulation Using Ptolemy II , , 2014 . . 2020 http://ptolemy.org/books/Systems http://ptolemy.org/books/Systems , , [Accessed on Aug. 30, 2020] . .
ZJ Qin , , , N Do , , , G Denker , , , 等 . . Software-defined cyber-physical multinetworks . . Int Conf on Computing, Networking and Communications , , 2014 . . p.322 - - 326 . . DOI: 10.1109/ICCNC.2014.6785354 http://doi.org/10.1109/ICCNC.2014.6785354 . .
LA Rahim , , , J Whittle . . A survey of approaches for verifying model transformations . . Softw Syst Model , , 2015 . . 14 ( ( 2 ): ): 1003 - - 1028 . . DOI: 10.1007/s10270-013-0358-0 http://doi.org/10.1007/s10270-013-0358-0 . .
R Rajkumar , , , I Lee , , , L Sha , , , 等 . . Cyber-physical systems: the next computing revolution . . Design Automation Conf , , 2010 . . p.731 - - 736 . . DOI: 10.1145/1837274.1837461 http://doi.org/10.1145/1837274.1837461 . .
N Saeedloei , , , G Gupta . . A methodology for modeling and verification of cyber-physical systems based on logic programming . . ACM SIGBED Rev , , 2016 . . 13 ( ( 2 ): ): 34 - - 42 . . DOI: 10.1145/2930957.2930963 http://doi.org/10.1145/2930957.2930963 . .
A Sangiovanni-Vincentelli , , , W Damm , , , R Passerone . . Taming Dr~Frankenstein: contract-based design for cyber-physical systems . . Eur J Contr , , 2012 . . 18 ( ( 3 ): ): 217 - - 238 . . DOI: 10.3166/ejc.18.217-238 http://doi.org/10.3166/ejc.18.217-238 . .
E Seidewitz . . What models mean . . IEEE Softw , , 2003 . . 20 ( ( 5 ): ): 26 - - 32 . . DOI: 10.1109/MS.2003.1231147 http://doi.org/10.1109/MS.2003.1231147 . .
B Selic . . The pragmatics of model-driven development . . IEEE Softw , , 2003 . . 20 ( ( 5 ): ): 19 - - 25 . . DOI: 10.1109/MS.2003.1231146 http://doi.org/10.1109/MS.2003.1231146 . .
B Selić , , , S Gérard . . Modeling and Analysis of Real-Time and Embedded Systems with UML and MARTE . . Elsevier, Amsterdam , , 2014 . . DOI: 10.1016/C2012-0-13536-5 http://doi.org/10.1016/C2012-0-13536-5 . .
L Sha , , , S Gopalakrishnan , , , X Liu , , , 等 . . Cyber-physical systems: a new frontier . . Int Conf on Sensor Networks, Ubiquitous, and Trustworthy Computing , , 2008 . . p.1 - - 9 . . DOI: 10.1109/SUTC.2008.85 http://doi.org/10.1109/SUTC.2008.85 . .
G Simko , , , T Levendovszky , , , M Maroti , , , 等 . . Towards a theory for cyber-physical systems modeling . . Proc $4^{\rm th}$ ACM SIGBED Int Workshop on Design, Modeling, and Evaluation of Cyber-Physical Systems , , 2014 . . p.56 - - 61 . . DOI: 10.1145/2593458.2593463 http://doi.org/10.1145/2593458.2593463 . .
Y Tan , , , MC Vuran , , , S Goddard . . Spatio-temporal event model for cyber-physical systems . . Proc $29^{\rm th}$ IEEE Int Conf on Distributed Computing Systems Workshops , , 2009 . . p.44 - - 50 . . DOI: 10.1109/ICDCSW.2009.82 http://doi.org/10.1109/ICDCSW.2009.82 . .
MU Tariq , , , S Grijalva , , , M Wolf . . A service-oriented, cyber-physical reference model for smart grid.In: Khaitan SK, McCalley JD, Liu CC (Eds.), Cyber Physical Systems Approach to Smart Electric Power Grid . . Springer, Berlin , , 2015 . . p.25 - - 42 . . . .
The Object Management Group . . Meta-data Interchange (XMI) Specification , , 2000 . . 2020 https://www.omg.org/spec/QVT/1.0/PDF https://www.omg.org/spec/QVT/1.0/PDF , , [Accessed on Aug. 30, 2020] . .
The Object Management Group . . Model Driven Architecture , , 2006 . . 2020 http://www.omg.org/mda/ http://www.omg.org/mda/ , , [Accessed on Aug. 30, 2020] . .
The Object Management Group . . Meta Object Facility (MOF) 2.0 Query/View/Transformation Specification , , 2008 . . 2020 https://www.omg.org/spec/QVT/1.0/PDF https://www.omg.org/spec/QVT/1.0/PDF , , [Accessed on Aug. 30, 2020] . .
The Object Management Group . . Business Process Model and Notation (BPMN) Version 2.0.2 , , 2013 . . .
L Tratt . . Model transformations and tool integration . . Softw Syst Model , , 2005 . . 4 ( ( 2 ): ): 112 - - 122 . . DOI: 10.1007/s10270-004-0070-1 http://doi.org/10.1007/s10270-004-0070-1 . .
D Varró , , , A Balogh . . The model transformation language of the VIATRA2 framework . . Sci Comput Program , , 2007 . . 68 ( ( 3 ): ): 214 - - 234 . . DOI: 10.1016/j.scico.2007.05.004 http://doi.org/10.1016/j.scico.2007.05.004 . .
D Varró , , , A Pataricza . . VPM: a visual, precise and multilevel metamodeling framework for describing mathematical domains and UML (The Mathematics of Metamodeling is Metamodeling Mathematics) . . Softw Syst Model , , 2003 . . 2 ( ( 3 ): ): 187 - - 210 . . DOI: 10.1007/s10270-003-0028-8 http://doi.org/10.1007/s10270-003-0028-8 . .
BB Wang , , , JS Baras . . HybridSim: a modeling and co-simulation toolchain for cyber-physical systems . . $17 ^{\rm th}$ IEEE/ACM Int Symp on Distributed Simulation and Real Time Applications , , 2013 . . p.33 - - 40 . . DOI: 10.1109/DS-RT.2013.12 http://doi.org/10.1109/DS-RT.2013.12 . .
J Wang , , , NJ Zhan , , , XY Feng , , , 等 . . Overview of formal methods . . J Softw , , 2019 . . 30 ( ( 1 ): ): 33 - - 61 . . DOI: 10.13328/j.cnki.jos.005652 http://doi.org/10.13328/j.cnki.jos.005652 . .
SL Wang , , , NJ Zhan , , , L Zou . . An improved HHL prover: an interactive theorem prover for hybrid systems . . Proc $17^{\rm th}$ Int Conf on Formal Engineering Methods on Formal Methods and Software Engineering , , 2015 . . p.382 - - 399 . . DOI: 10.1007/978-3-319-25423-4_25 http://doi.org/10.1007/978-3-319-25423-4_25 . .
TX Wang , , , S Truptil , , , F Benaben . . An automatic model-to-model mapping and transformation methodology to serve model-based systems engineering . . Inform Syst E-Bus Manag , , 2017 . . 15 ( ( 2 ): ): 323 - - 376 . . DOI: 10.1007/s10257-016-0321-z http://doi.org/10.1007/s10257-016-0321-z . .
W3C . . W3C Recommendation , , 1999 . . https://www.w3.org/TR/1999/REC-xslt-19991116 https://www.w3.org/TR/1999/REC-xslt-19991116 , , . .
B Xue , , , ZK She , , , A Easwaran . . Under-approximating backward reachable sets by polytopes . . Proc $28^{\rm th}$ Int Conf on Computer Aided Verification , , 2016 . . p.457 - - 476 . . DOI: 10.1007/978-3-319-41528-4_25 http://doi.org/10.1007/978-3-319-41528-4_25 . .
B Xue , , , PN Mosaad , , , M Fränzle , , , 等 . . Safe over- and under-approximation of reachable sets for delay differential equations . . $15^{\rm th}$ Int Conf on Formal Modeling and Analysis of Timed Systems , , 2017 . . p.97 - - 115 . . DOI: 10.1007/978-3-319-65765-3_16 http://doi.org/10.1007/978-3-319-65765-3_16 . .
AB Younes , , , YB Hlaoui , , , LJB Ayed . . A meta-model transformation from UML activity diagrams to Event-B models . . Proc IEEE $38^{\rm th}$ Int Computer Software and Applications Conf Workshops , , 2014 . . p.740 - - 745 . . DOI: 10.1109/COMPSACW.2014.119 http://doi.org/10.1109/COMPSACW.2014.119 . .
NJ Zhan , , , SL Wang , , , HJ Zhao . . Formal Verification of Simulink/Stateflow Diagrams: a Deductive Approach . . Springer, Cham , , 2016 . . p.1 - - 258 . . . .
LC Zhang , , , SG Feng . . Aspect-oriented QoS modeling of cyber-physical systems by the extension of architecture analysis and design language . . Proc Int Conf on Computer Engineering and Network , , 2014 . . p.1125 - - 1131 . . DOI: 10.1007/978-3-319-01766-2_128 http://doi.org/10.1007/978-3-319-01766-2_128 . .
Publicity Resources
Related Articles
Related Author
Related Institution
京公网安备11010802024621