Page 298 - 《软件学报》2026年第3期

徐雄 等: 嵌入式软件 IP 通用模型 1261

[47] Konnov I, Kotek T, Wang Q, Veith H, Bliudze S, Sifakis J. Parameterized systems in BIP: Design and model checking. In: Proc. of the
27th Int’l Conf. on Concurrency Theory. Québec City: Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2016. 30. [doi: 10.4230/
LIPIcs.CONCUR.2016.30]
[48] Bozga M, Iosif R, Sifakis J. Checking deadlock-freedom of parametric component-based systems. Journal of Logical and Algebraic
Methods in Programming, 2021, 119: 100621. [doi: 10.1016/j.jlamp.2020.100621]
[49] He JF, Li XS, Liu ZM. Component-based software engineering. In: Proc. of the 2nd Int’l Colloquium on Theoretical Aspects of
Computing. Hanoi: Springer, 2005. 70–95. [doi: 10.1007/11560647_5]
[50] He JF, Li XS, Liu ZM. A theory of reactive components. Electronic Notes in Theoretical Computer Science, 2006, 160: 173–195. [doi:
10.1016/j.entcs.2006.05.022]
[51] He JF, Li XS, Liu ZM. rCOS: A refinement calculus of object systems. Theoretical Computer Science, 2006, 365(1–2): 109–142. [doi:
10.1016/j.tcs.2006.07.034]
[52] Chen X, He JF, Liu ZM, Zhan NJ. A model of component-based programming. In: Proc. of the 2007 Int’l Conf. on Fundamentals of
Software Engineering. Tehran: Springer, 2007. 191–206. [doi: 10.1007/978-3-540-75698-9_13]
[53] Zhan NJ, Kang EY, Liu ZM. Component publications and compositions. In: Proc. of the 2nd Int’l Symp. on Unifying Theories of
Programming. Dublin: Springer, 2008. 238–257. [doi: 10.1007/978-3-642-14521-6_14]
[54] Liebrenz T, Herber P, Glesner S. Deductive verification of hybrid control systems modeled in Simulink with KeYmaera X. In: Proc. of
the 20th Int’l Conf. on Formal Engineering Methods. Gold Coast: Springer, 2018. 89–105. [doi: 10.1007/978-3-030-02450-5_6]
[55] Herber P, Adelt J, Liebrenz T. Formal verification of intelligent cyber-physical systems with the interactive theorem prover KeYmaera
X. In: Proc. of the 2021 Software Engineering Satellite Events. Braunschweig: Software Engineering, 2021.
[56] Simko G, Lindecker D, Levendovszky T, Neema S, Sztipanovits J. Specification of cyber-physical components with formal
semantics—Integration and composition. In: Proc. of the 16th Int’l Conf. on Model Driven Engineering Languages and Systems. Miami:
Springer, 2013. 471–487. [doi: 10.1007/978-3-642-41533-3_29]
[57] Sztipanovits J, Bapty T, Koutsoukos X, Lattmann Z, Neema S, Jackson E. Model and tool integration platforms for cyber-physical
system design. Proc. of the IEEE, 2018, 106(9): 1501–1526. [doi: 10.1109/JPROC.2018.2838530]
[58] Meyer B. Applying ‘design by contract’. Computer, 1992, 25(10): 40–51. [doi: 10.1109/2.161279]
[59] Meyer B. Touch of class. Learning to program well with object technology and design by contract, an introduction to software
engineering. 2009. https://se.inf.ethz.ch/~meyer/down/touch/TOUCH.pdf
[60] Floyd RW. Assigning meanings to programs. Mathematical Aspects of Computer Science, 1967, 19: 19–32.
[61] Abadi M, Lamport L, Wolper P. Realizable and unrealizable specifications of reactive systems. In: Proc. of the 16th Int’l Colloquium on
Automata, Languages and Programming. Stresa: Springer, 1989. 1–17. [doi: 10.1007/BFb0035748]
[62] Abadi M, Lamport L. Composing specifications. ACM Trans. on Programming Languages and Systems (TOPLAS), 1993, 15(1):
73–132. [doi: 10.1145/151646.151649]
[63] de Alfaro L, Henzinger TA. Interface automata. ACM SIGSOFT Software Engineering Notes, 2001, 26(5): 109–120. [doi: 10.1145/
503271.503226]
[64] Chakrabarti A, de Alfaro L, Henzinger TA, Stoelinga M. Resource interfaces. In: Proc. of the 3rd Int’l Workshop on Embedded
Software. Philadelphia: Springer, 2003. 117–133. [doi: 10.1007/978-3-540-45212-6_9]
[65] Henzinger TA, Jhala R, Majumdar R. Permissive interfaces. In: Proc. of the 10th European Software Engineering Conf. Held Jointly
with 13th ACM SIGSOFT Int’l Symp. on Foundations of Software Engineering. Lisbon: ACM, 2005. 31–40. [doi: 10.1145/1081706.
1081713]
[66] Larsen KG, Nyman U, Wąsowski A. Interface input/output automata. In: Proc. of the 14th Int’l Symp. on Formal Methods. Hamilton:
Springer, 2006. 82–97. [doi: 10.1007/11813040_7]
[67] Reineke J, Tripakis S. Basic problems in multi-view modeling. In: Proc. of the 20th Int’l Conf. on Tools and Algorithms for the
Construction and Analysis of Systems. Grenoble: Springer, 2014. 217–232. [doi: 10.1007/978-3-642-54862-8_15]
[68] de Alfaro L, Henzinger TA, Stoelinga M. Timed interfaces. In: Proc. of the 2nd Int’l Workshop on Embedded Software. Grenoble:
Springer, 2002. 108–122. [doi: 10.1007/3-540-45828-X_9]
[69] David A, Larsen KG, Legay A, Nyman U, Wasowski A. Timed I/O automata: A complete specification theory for real-time systems. In:
Proc. of the 13th ACM Int’l Conf. on Hybrid Systems: Computation and Control. Stockholm: ACM, 2010. 91–100. [doi: 10.1145/
1755952.1755967]
[70] David A, Larsen KG, Legay A, Nyman U, Wąsowski A. ECDAR: An environment for compositional design and analysis of real time
systems. In: Proc. of the 8th Int’l Symp. on Automated Technology for Verification and Analysis. Singapore: Springer, 2010. 365–370.
[doi: 10.1007/978-3-642-15643-4_29]
[71] Bertrand N, Pinchinat S, Raclet JB. Refinement and consistency of timed modal specifications. In: Proc. of the 3rd Int’l Conf. on