首页 | 本学科首页   官方微博 | 高级检索  
     


Real-time system = discrete system + clock variables
Authors:Rajeev Alur  Thomas A.
Affiliation:(1) CIS Department, University of Pennsylvania, Philadelphia, PA 19104, USA; E-mail: alur@cis.upenn.edu, US;(2) EECS Department, University of California, Berkeley, CA 94720, USA; E-mail: tah@eecs.berkeley.edu, US
Abstract:This paper introduces, gently but rigorously, the clock approach to real-time programming. We present with mathematical precision, assuming no prerequisites other than familiarity with logical and programming notations, the concepts that are necessary for understanding, writing, and executing clock programs. In keeping with an expository style, all references are clustered in bibliographic remarks at the end of each section. The first appendix presents proof rules for verifying temporal properties of clock programs. The second appendix points to selected literature on formal methods and tools for programming with clocks. In particular, the timed automaton, which is a finite-state machine equipped with clocks, has become a standard paradigm for real-time model checking; it underlies the tools HyTech, Kronos, and Uppaal, which are discussed elsewhere in this volume.
Keywords:: Real-time systems –   Real-time programs –   Clock variables –   Semantics and verification
本文献已被 SpringerLink 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号