Modeling and verification of hybrid systems based on equations

被引：0
|
作者：
Ogata, K
Yamagishi, D
Seino, T
Futatsugi, K
机构：
来源：
DESIGN METHODS AND APPLICATIONS FOR DISTRIBUTED EMBEDDED SYSTEMS | 2004年 / 150卷
关键词：
CafeOBJ; HOTS; hybrid systems; modeling; verification;
D O I：
暂无
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
We describe hybrid observational transition systems, or HOTSs. HOTSs are written in terms of equations and verified by means of equational reasoning. More concretely, CafeOBJ, an algebraic specification language, is used to specify HOTSs and verify that HOTSs have properties by writing proofs, or proof scores. One case study is used to demonstrate how to model hybrid systems as HOTSs, specify HOTSs in CafeOBJ and verify that HOTSs have properties with the CafeOBJ system.
引用
收藏
页码：43 / 52
页数：10
相关论文
共 50 条
  • [1] Modeling and verification of real-time systems based on equations
    Ogata, Kazuhiro
    Futatsugi, Kokichi
    SCIENCE OF COMPUTER PROGRAMMING, 2007, 66 (02) : 162 - 180
  • [2] Hybrid modeling and verification of embedded control systems
    Mosterman, PJ
    Biswas, G
    Sztipanovits, J
    COMPUTER AIDED CONTROL SYSTEMS DESIGN (CACSD'97), 1997, : 33 - 38
  • [3] A hybrid modeling and verification paradigm for embedded control systems
    Mosterman, PJ
    Biswas, G
    Sztipanovits, J
    CONTROL ENGINEERING PRACTICE, 1998, 6 (04) : 511 - 521
  • [4] Modeling and verification of distributed real-time systems based on CafeOBJ
    Ogata, K
    Futatsugi, K
    16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS, 2001, : 185 - 192
  • [5] Mediation systems modeling and verification
    Yang, L
    Ege, RK
    Yu, HQ
    ICECCS 2005: 10TH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2005, : 322 - 331
  • [6] Current Challenges in the Verification of Hybrid Systems
    Schupp, Stefan
    Abraham, Erika
    Chen, Xin
    Ben Makhlouf, Ibtissem
    Frehse, Goran
    Sankaranarayanan, Sriram
    Kowalewski, Stefan
    CYBER PHYSICAL SYSTEMS: DESIGN, MODELING, AND EVALUATION, CYPHY 2015, 2015, 9361 : 8 - 24
  • [7] Computational techniques for the verification of hybrid systems
    Tomlin, CJ
    Mitchell, I
    Bayen, AM
    Oishi, M
    PROCEEDINGS OF THE IEEE, 2003, 91 (07) : 986 - 1001
  • [8] Safety verification of hybrid systems by constraint propagation-based abstraction refinement
    Ratschan, Stefan
    She, Zhikun
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2007, 6 (01) : 8
  • [9] Modeling and verification of CPS based on uncertain hybrid timed automaton
    Chen, Na
    Geng, Shengling
    Li, Lin
    2021 IEEE INTL CONF ON DEPENDABLE, AUTONOMIC AND SECURE COMPUTING, INTL CONF ON PERVASIVE INTELLIGENCE AND COMPUTING, INTL CONF ON CLOUD AND BIG DATA COMPUTING, INTL CONF ON CYBER SCIENCE AND TECHNOLOGY CONGRESS DASC/PICOM/CBDCOM/CYBERSCITECH 2021, 2021, : 971 - 978
  • [10] Recursive and backward reasoning in the verification on hybrid systems
    Ratschan, Stefan
    She, Zhikun
    ICINCO 2008: PROCEEDINGS OF THE FIFTH INTERNATIONAL CONFERENCE ON INFORMATICS IN CONTROL, AUTOMATION AND ROBOTICS, VOL SPSMC: SIGNAL PROCESSING, SYSTEMS MODELING AND CONTROL, 2008, : 65 - +
12345