Real-time Systems-oriented Real-time Regional Temporal Logic: Rrtl

As an important reactive systems, real-time systems has been used widely in safety-critical field, so it's safety and reliability must been guaranteed. In order to satisfy this requirement, formal method which is based on precise mathematical foundation must been used. In this thesis, schematic summary about formal method is presented. Furthermore, an overview about real-time systems which is different from generic reactive systems is given. We review real time extension of formal method oriented real time system.In order to specify real-time system, many real time-logic, such as Metric Interval Temporal Logic, Real Time Temporal Logic, Timed Propositional Temporal Logic have been proposed. We reviewed a selection of most representative real-time logic. Neither real-time logics based point-semantic nor real-time logics based interval-semantic is intuitionistic for specifying real-time systems, especially for real time systems which events occurs repeatedly.In respect that, the concept of region which is made up of infinite interval sequence is introduced. Based on this, unary operation about region and binary relationship between region is defined. A Real-time Region Temporal Logic, called RRTL,is introduced. It is an extension of core of Manna and Pnueli 's PLTL.In succession, a formal axiom deductive system is presented. It's soundness based formal semantic defined in this thesis is proved. As an example, We specify GRC(Generalized Railroad Crossing) ,which is a benchmark problem for real time systems, and verify it's safety and liveness. In the end , a tool developed by us which is used for region reasoning is introduced.