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 条
  • [31] Design Flow for Hybrid CMOS/Memristor Systems-Part I: Modeling and Verification Steps
    Maheshwari, Sachin
    Stathopoulos, Spyros
    Wang, Jiaqi
    Serb, Alexander
    Pan, Yihan
    Mifsud, Andrea
    Leene, Lieuwe B.
    Shen, Jiawei
    Papavassiliou, Christos
    Constandinou, Timothy G.
    Prodromakis, Themistoklis
    IEEE TRANSACTIONS ON CIRCUITS AND SYSTEMS I-REGULAR PAPERS, 2021, 68 (12) : 4862 - 4875
  • [32] Modeling hybrid systems in Scicos: A case study
    Nikoukhah, R
    Proceedings of the 25th IASTED International Conference on Modelling, Identification, and Control, 2006, : 315 - 319
  • [33] Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations
    Botchkarev, O
    Tripakis, S
    HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2000, 1790 : 73 - 88
  • [34] Discrete-time hybrid modeling and verification of the batch evaporator process benchmark
    Bemporad, A
    Torrisi, FD
    Morari, M
    EUROPEAN JOURNAL OF CONTROL, 2001, 7 (04) : 382 - 399
  • [35] Modeling and Verification of a Robotic Surgical System using Hybrid Input/Output Automata
    Capiluppi, Marta
    Schreiter, Luzie
    Fiorini, Paolo
    Raczkowsky, Joerg
    Woern, Heinz
    2013 EUROPEAN CONTROL CONFERENCE (ECC), 2013, : 4238 - 4243
  • [36] SMT-Based Modeling and Verification of Cloud Applications
    Zhang, Xiyue
    Sun, Meng
    SERVICES - SERVICES 2019, 2019, 11517 : 1 - 15
  • [37] Symbolic verification of hybrid systems: An algebraic approach
    von Mohrenschildt, M
    EUROPEAN JOURNAL OF CONTROL, 2001, 7 (05) : 541 - 556
  • [38] Computational methods for verification of stochastic hybrid systems
    Koutsoukos, Xenofon D.
    Riley, Derek
    IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2008, 38 (02): : 385 - 396
  • [39] MLD-Based Modeling of Hybrid Systems with Parameter Uncertainty
    Kobayashi, Koichi
    Hiraishi, Kunihiko
    IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 2009, E92A (11) : 2745 - 2754
  • [40] Measurability and Safety Verification for Stochastic Hybrid Systems
    Fraenzle, Martin
    Hahn, Ernst Moritz
    Hermanns, Holger
    Wolovick, Nicolas
    Zhang, Lijun
    HSCC 11: PROCEEDINGS OF THE 14TH INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2011, : 43 - 52
12345