Compositional verification of real-time applications

被引:0
|
作者
Hooman, J [1 ]
机构
[1] Eindhoven Univ Technol, Dept Comp Sci, NL-5600 MB Eindhoven, Netherlands
关键词
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
To support top-down design of distributed real-time systems, a framework of mixed terms has been incorporated in the verification system PVS. Programs and assertional specifications are treated in a uniform way. We focus on the timed behaviour of parallel composition and hiding, presenting several alternatives for the definition of a denotational semantics. This forms the basis of compositional proof rules for parallel composition and hiding. The formalism is applied to an example of a hybrid system, which also serves to illustrate our ideas on platform independent programming.
引用
收藏
页码:276 / 300
页数:25
相关论文
共 50 条
  • [21] Compositional Model Checking for Real-Time Systems
    Hou, J.
    Li, X.
    Fan, X.
    Zheng, G.
    Software Engineering Notes, 23 (01):
  • [22] COMPOSITIONAL SEMANTICS FOR REAL-TIME DISTRIBUTED COMPUTING
    KOYMANS, R
    SHYAMASUNDAR, RK
    DEROEVER, WP
    GERTH, R
    ARUNKUMAR, S
    INFORMATION AND COMPUTATION, 1988, 79 (03) : 210 - 256
  • [23] Real-time compositional analysis of submicrometre particles
    Reents, W. D., Jr.
    Downey, S. W.
    Emerson, A. B.
    Mujsce, A. M.
    Muller, A. J.
    Siconolfi, D. J.
    Sinclair, J. D.
    Swanson, A. G.
    PLASMA SOURCES SCIENCE & TECHNOLOGY, 1994, 3 (03): : 369 - 372
  • [24] A framework for compositional and hierarchical real-time scheduling
    Marimuthu, Shanmuga Priya
    Chakraborty, Samarjit
    12TH IEEE INTERNATIONAL CONFERENCE ON EMBEDDED AND REAL-TIME COMPUTING SYSTEMS AND APPLICATIONS, PROCEEDINGS, 2006, : 91 - +
  • [25] Automated compositional proofs for real-time systems
    Furia, Carlo A.
    Rossi, Matteo
    Mandrioli, Dino
    Morzenti, Angelo
    THEORETICAL COMPUTER SCIENCE, 2007, 376 (03) : 164 - 184
  • [26] A compositional real-time semantics of STATEMATE designs
    Damm, W
    Josko, B
    Hungar, H
    Pnueli, A
    COMPOSITIONALITY: THE SIGNIFICANT DIFFERENCE, 1998, 1536 : 186 - 238
  • [27] Compositional Analysis of Real-Time Embedded Systems
    Phan, Linh T. X.
    Lee, Insup
    Sokolsky, Oleg
    PROCEEDINGS OF THE PROCEEDINGS OF THE 14TH INTERNATIONAL CONFERENCE ON COMPILERS, ARCHITECTURES AND SYNTHESIS FOR EMBEDDED SYSTEMS (CASES '11), 2011, : 237 - 238
  • [28] A compositional framework for real-time embedded systems
    Shin, I
    Lee, I
    SERVICE AVAILABILITY, 2005, 3694 : 137 - 148
  • [29] COMPOSITIONAL SEMANTICS OF A REAL-TIME PROTOTYPING LANGUAGE
    KRAMER, B
    LUQI
    BERZINS, V
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1993, 19 (05) : 453 - 477
  • [30] Virtual scheduling for compositional real-time guarantees
    van den Heuvel, Martijn M. H. P.
    Bril, Reinder J.
    Lukkien, Johan J.
    2013 8TH IEEE INTERNATIONAL SYMPOSIUM ON INDUSTRIAL EMBEDDED SYSTEMS (SIES), 2013, : 151 - 160