Transformation-Based Reactive Systems Development: 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ... Spain, May 21 - 23, 1997, Proceedings

by Miquel Bertran (editor)

What was Llull up to?.- Llull as computer scientist or why Llull was one of us.- Deductive verification of real-time systems using STeP.- Refinement of Time.- The verus Representing time efficiently with BDDs.- Refining interval temporal logic specifications.- Integrating temporal logics and model checking algorithms.- A new class of implementable real-time automata.- Communication concepts for A semantic foundation.- Regular processes and timed automata.- A visual formalism for real time requirement specifications.- Formal specification and verification method of concurrent and distributed systems by restricted timed automata.- Transformational formal development of real-time systems.- A transformation of monitor into communication synchronized parallel A systematic refinement step in design.- Contracts for ODP.- Affine transformations in Signal and their application in the specification and validation of real-time systems.- Action-based concurrency and synchronization for objects.- Communication Extended Abstract Types in the refinement of parallel communicating processes.- Verification and refinement of distributed programs in a fair framework.- Formalizing real-time scheduling as program refinement.- Specification and refinement of continuous real-time systems.- High-level execution time analysis.- A sound and complete proof system for probabilistic processes.- Testing semantics for a probabilistic-timed process algebra.- Denotational semantics for timed testing.- Extending LOTOS with A true concurrency perspective.- of a suspend/resume operator in ET-LOTOS.- Specification and verification of a real-time field bus with formal description languages.

452 pages, Paperback

First published June 13, 1997