A Denotational Semantics of Real-Time Process Algebra (RTPA)

被引:3
作者
Tan, Xinming [1 ,2 ]
Wang, Yingxu [1 ]
机构
[1] Univ Calgary, Software Engn, Calgary, AB, Canada
[2] Wuhan Univ Technol, Sch Comp Sci & Technol, Wuhan, Peoples R China
基金
加拿大自然科学与工程研究理事会;
关键词
cognitive informatics; deductive semantics; denotationalmathematics; denotationalsemantics; formal methods; formal semantics; RTPA; real-time systems; software engineering;
D O I
10.4018/jcini.2008070105
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
Real-time process algebra (RIM) is a form of denotational mathematics far dealing with fundamental system behaviors such as timing, internfp', concurrency, and event/time/interrupt-driven system dispatching. Because some key RIPilproce.sses cannot be described adequately in conventional denotational semantic paradigms, a new frameworkfOrmodeling time and processes is sought in order to represent RTP4 in denotational semantics. Within this framework, time is modeled by the elapse ofprocess execution. The process environment encompasses states ofall variables represented as mathematical maps, which project variables to their corresponding values. Duration is introduced as a pair of time intervals and the environment to represent the changes ofthe.process environment during a time interval. Temporal ordered durations and operations on them are used to denote process executions. On the basis of these means, a comprehensive set of denotational semantics for RTPA are systematically developed and formally expressed.
引用
收藏
页码:57 / 70
页数:14
相关论文
共 50 条
[31]   VISUAL METHODS IN REAL-TIME PROGRAMMING [J].
HINCHEY, MG .
CONTROL ENGINEERING PRACTICE, 1995, 3 (06) :837-842
[32]   Compounded Real-Time Operating Systems for Rich Real-Time Applications [J].
Yang, Chung-Fan ;
Shinjo, Yasushi .
IEEE ACCESS, 2025, 13 :26079-26104
[33]   A survey of formal verification methods and tools for embedded and real-time systems [J].
Cheng, Albert Mo Kim .
INTERNATIONAL JOURNAL OF EMBEDDED SYSTEMS, 2006, 2 (3-4) :184-195
[34]   Metric semantics for true concurrent real time [J].
Katoen, JP ;
Baier, C ;
Latella, D .
THEORETICAL COMPUTER SCIENCE, 2001, 254 (1-2) :501-542
[35]   A Real-Time Quality Control System Based on Manufacturing Process Data [J].
Duan, Gui-Jiang ;
Yan, Xin .
IEEE ACCESS, 2020, 8 :208506-208517
[36]   Real-time specifications [J].
Alexandre David ;
Kim G. Larsen ;
Axel Legay ;
Ulrik Nyman ;
Louis-Marie Traonouez ;
Andrzej Wąsowski .
International Journal on Software Tools for Technology Transfer, 2015, 17 :17-45
[37]   Real-time specifications [J].
David, Alexandre ;
Larsen, Kim G. ;
Legay, Axel ;
Nyman, Ulrik ;
Traonouez, Louis-Marie ;
Wasowski, Andrzej .
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2015, 17 (01) :17-45
[38]   Formal description of time management in real-time operating systems [J].
Rusu-Banu, Fabricio ;
Wang, Yingxu .
2006 CANADIAN CONFERENCE ON ELECTRICAL AND COMPUTER ENGINEERING, VOLS 1-5, 2006, :1801-+
[39]   A generic component framework for real-time control [J].
Griph, FS ;
Hogben, CHA ;
Buckley, MA .
IEEE TRANSACTIONS ON NUCLEAR SCIENCE, 2004, 51 (03) :558-564
[40]   A scalable method for testing real-time systems [J].
En-Nouaary, Abdeslam .
SOFTWARE QUALITY JOURNAL, 2008, 16 (01) :3-22