Conference paper

JANKOVSKÝ Michal and ŠVÉDA Miroslav. From TLA Specifications to Real-Time Unix Applications. In: Proceedings IEEE/IFIP Joint Workshop on Formal Specification of CBS. Napier University, Edinburgh: unknown, 2000, pp. 77-79. ISBN 1-85-769121-0.
Publication language:english
Original title:From TLA Specifications to Real-Time Unix Applications
Title (cs):From TLA Specifications to Real-Time Unix Applications
Pages:77-79
Proceedings:Proceedings IEEE/IFIP Joint Workshop on Formal Specification of CBS
Conference:IEEE TC-ECBS + TF RE and IFIP WG10.1 Joint Workshop on Formal Specifications of Computer-Based Systems
Place:Napier University, Edinburgh, GB
Year:2000
ISBN:1-85-769121-0
Keywords
real-time, POSIX.4, POSIX.4a, TLA
Annotation
The paper presents a method that utilizes formal specifications both for design of soft real-time (RT) systems, and for their implementation aimed at RT Unix portable operating systems environments defined by the POSIX.4 and POSIX.4a standards. The method stems from the following contributions: (i) extension of the Temporal Logic of Actions (TLA) by time-bounded temporal operators for straightforward specifications of RT systems, and (ii) concept of the executive engine that provides services for effective and correct execution of actions according to their specification. The method was employed to develop the Tower Simulation Module of an airport-tower crew training courseware, which is based on the LynxOS operating system.
BibTeX:
@INPROCEEDINGS{
   author = {Michal Jankovsk{\'{y}} and Miroslav {\v{S}}v{\'{e}}da},
   title = {From TLA Specifications to Real-Time Unix Applications},
   pages = {77--79},
   booktitle = {Proceedings IEEE/IFIP Joint Workshop on Formal Specification
	of CBS},
   year = {2000},
   location = {Napier University, Edinburgh, GB},
   ISBN = {1-85-769121-0},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=6506}
}

Your IPv4 address: 54.158.55.5
Switch to IPv6 connection

DNSSEC [dnssec]