Specifying and Verifying Real-Time Systems using Second-Order Algebraic Methods: A Case Study of the Railroad Crossing Controller
| dc.creator | Steggles,L. | |
| dc.date | 2000 | |
| dc.date.accessioned | 2024-02-06T12:50:33Z | |
| dc.date.available | 2024-02-06T12:50:33Z | |
| dc.description | Second-order algebraic methods provide a natural and expressive formal framework in which to develop correct computing systems. In this paper we consider using second-order algebraic methods to specify real-time systems and to verify their associated safety and utility properties. We demonstrate our ideas by presenting a detailed case study of the railroad crossing controller, a benchmark example in the real-time systems community. This case study demonstrates how real-time constraints can be modelled naturally using second-order algebras and illustrates the substantial expressive power of second-order equations. | |
| dc.format | text/html | |
| dc.identifier | https://doi.org/10.3217/jucs-006-04-0460 | |
| dc.identifier | https://lib.jucs.org/article/27673/ | |
| dc.identifier.uri | https://openrepository.mephi.ru/handle/123456789/7745 | |
| dc.language | en | |
| dc.publisher | Journal of Universal Computer Science | |
| dc.relation | info:eu-repo/semantics/altIdentifier/eissn/0948-6968 | |
| dc.relation | info:eu-repo/semantics/altIdentifier/pissn/0948-695X | |
| dc.rights | info:eu-repo/semantics/openAccess | |
| dc.rights | J.UCS License | |
| dc.source | JUCS - Journal of Universal Computer Science 6(4): 460-473 | |
| dc.subject | real-time systems | |
| dc.subject | algebraic specification methods | |
| dc.subject | formal verification | |
| dc.title | Specifying and Verifying Real-Time Systems using Second-Order Algebraic Methods: A Case Study of the Railroad Crossing Controller | |
| dc.type | Research Article |