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 条
  • [31] A Compositional Approach for Real-Time Machine Learning
    Allen, Nathan
    Raje, Yash
    Ro, Jin Woo
    Roop, Partha
    17TH ACM-IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR SYSTEM DESIGN (MEMOCODE), 2019,
  • [32] Compositional Construction of Real-Time Dataflow Networks
    Kemper, Stephanie
    COORDINATION MODELS AND LANGUAGES, PROCEEDINGS, 2010, 6116 : 92 - 106
  • [33] A typed compositional language for real-time systems
    Etienne, Jean-Paul
    Bouzefrane, Samia
    HASE 2007: 10TH IEEE HIGH ASSURANCE SYSTEMS ENGINEERING SYMPOSIUM, PROCEEDINGS, 2007, : 63 - +
  • [34] Compositional Abstraction in Real-Time Model Checking
    Berendsen, Jasper
    Vaandrager, Frits
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, PROCEEDINGS, 2008, 5215 : 233 - 249
  • [35] Automated compositional proofs for real-time systems
    Furia, CA
    Rossi, M
    Mandrioli, D
    Morzenti, A
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2005, 3442 : 326 - 340
  • [36] REAL-TIME FINGERPRINT VERIFICATION SYSTEM
    GAMBLE, FT
    FRYE, LM
    GRIESER, DR
    APPLIED OPTICS, 1992, 31 (05): : 652 - 655
  • [37] An abstraction technique for real-time verification
    Clarke, Edmund M.
    Lerda, Flavio
    Talupur, Muralidhar
    NEXT GENERATION DESIGN AND VERIFICATION METHODOLOGIES FOR DISTRIBUTED EMBEDDED CONTROL SYSTEMS, 2007, : 1 - +
  • [38] TEMPORAL VERIFICATION OF REAL-TIME SYSTEMS
    CAMPOS, SV
    CLARKE, EM
    MARRERO, W
    MINEA, M
    HIRAISHI, H
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 1995, E78D (07) : 796 - 801
  • [39] Real-time speaker identification and verification
    Kinnunen, T
    Karpov, E
    Fränti, P
    IEEE TRANSACTIONS ON AUDIO SPEECH AND LANGUAGE PROCESSING, 2006, 14 (01): : 277 - 288
  • [40] A Real-Time Antenna Verification System
    Cutajar, D.
    Farhat, I.
    Magro, A.
    Borg, J.
    Adami, K. Zarb
    Sammut, C. V.
    2018 2ND URSI ATLANTIC RADIO SCIENCE MEETING (AT-RASC), 2018,