Steen, M.W.A. and Bowman, H. and Derrick, J. and Boiten, E.A. (1997) Disjunction of LOTOS specifications. In: Mizuno, Tadanori and Shiratori, Norio and Higashino, Teruo and Togashi, Atsushi, eds. Formal Description Techniques and Protocol Specification, Testing and Verification. IFIP - The International Federation for Information Processing . Springer, Boston, Massachusetts, USA, pp. 177-192. ISBN 978-1-4757-5260-1. E-ISBN 978-0-387-35271-8. (doi:10.1007/978-0-387-35271-8_11) (KAR id:21439)
PDF
Language: English |
|
Download this file (PDF/194kB) |
Preview |
Request a format suitable for use with assistive technology e.g. a screenreader | |
Official URL: http://dx.doi.org/10.1007/978-0-387-35271-8_11 |
Abstract
LOTOS is a formal specification language, designed for the precise description of open distributed systems and protocols. The definition of, so called, implementation relations has made it possible also to use LOTOS as a specification technique for the design of such systems. These LOTOS based specification techniques usually (ab)use non-determinism to achieve implementation freedom. Unfortunately, this is unsatisfactory when specifying non-deterministic processes. We, therefore, propose to extend LOTOS with a disjunction operator in order to achieve more implementation freedom while maintaining the possibility to describe non-deterministic processes. In contrast with similar proposals we maintain the operational semantics.
Item Type: | Book section |
---|---|
DOI/Identification number: | 10.1007/978-0-387-35271-8_11 |
Uncontrolled keywords: | LOTOS, process algebra, specification, disjunction, operational semantics |
Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Eerke Boiten |
Date Deposited: | 02 Aug 2009 21:28 UTC |
Last Modified: | 05 Nov 2024 09:59 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/21439 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):