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 条
  • [21] EMERALD: An Automated Modeling and Verification Tool for Component-Based Real-Time Systems
    Zhang, Yizhou
    Lin, Hao
    Li, Guoqiang
    2012 12TH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE (QSIC), 2012, : 120 - 123
  • [22] Exact Safety Verification of Hybrid Systems Based on Bilinear SOS Representation
    Yang, Zhengfeng
    Lin, Wang
    Wu, Min
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2015, 14 (01)
  • [23] ACTL strong negation and its application to hybrid systems verification
    Han, Zhi
    Chutinan, Alongkrit
    Krogh, Bruce H.
    CONTROL ENGINEERING PRACTICE, 2006, 14 (10) : 1259 - 1267
  • [24] An experimental batch plant as a test case for the verification of hybrid systems
    Kowalewski, S
    Stursberg, O
    Bauer, N
    EUROPEAN JOURNAL OF CONTROL, 2001, 7 (04) : 366 - 381
  • [25] Assume-guarantee verification of nonlinear hybrid systems with ARIADNE
    Benvenuti, Luca
    Bresolin, Davide
    Collins, Pieter
    Ferrari, Alberto
    Geretti, Luca
    Villa, Tiziano
    INTERNATIONAL JOURNAL OF ROBUST AND NONLINEAR CONTROL, 2014, 24 (04) : 699 - 724
  • [26] An assessment of the current status of algorithmic approaches to the verification of hybrid systems
    Silva, BI
    Stursberg, O
    Krogh, BH
    Engell, S
    PROCEEDINGS OF THE 40TH IEEE CONFERENCE ON DECISION AND CONTROL, VOLS 1-5, 2001, : 2867 - 2874
  • [27] Modeling Petri nets as local constraint equations for hybrid systems using Modelica™
    Mosterman, PJ
    Otter, M
    Elmqvist, H
    PROCEEDINGS OF THE 1998 SUMMER COMPUTER SIMULATION CONFERENCE: SIMULATION AND MODELING TECHNOLOGY FOR THE TWENTY-FIRST CENTURY, 1998, : 314 - 319
  • [28] Modeling and Verification of B-based Distributed Reconfigurable Control Systems
    Oueslati, Raja
    Mosbahi, Olfa
    Khalgui, Mohamed
    Ben Ahmed, Samir
    PECCS 2015 Proceedings of the 5th International Conference on Pervasive and Embedded Computing and Communication Systems, 2015, : 124 - 131
  • [29] Toward Modeling and Verification of Uncertainty in Cyber-Physical Systems
    Chatterjee, Amrita
    Reza, Hassan
    2020 IEEE INTERNATIONAL CONFERENCE ON ELECTRO INFORMATION TECHNOLOGY (EIT), 2020, : 568 - 576
  • [30] Modeling and formal verification of embedded systems based on a Petri net representation
    Cortés, LA
    Eles, P
    Peng, Z
    JOURNAL OF SYSTEMS ARCHITECTURE, 2003, 49 (12-15) : 571 - 598
12345