Transformation-Based Reactive Systems Development: 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS'97 Palma, Mallorca, Spain, May 21–23, 1997 Proceedings

What was Llull up to?....Pages 1-14
Llull as computer scientist or why Llull was one of us....Pages 15-21
Deductive verification of real-time systems using STeP....Pages 22-43
Refinement of Time....Pages 44-63
The verus language: Representing time efficiently with BDDs....Pages 64-78
Refining interval temporal logic specifications....Pages 79-94
Integrating temporal logics and model checking algorithms....Pages 95-110
PLC-automata: A new class of implementable real-time automata....Pages 111-125
Communication concepts for statecharts: A semantic foundation....Pages 126-140
Regular processes and timed automata....Pages 141-155
A visual formalism for real time requirement specifications....Pages 156-168
Formal specification and verification method of concurrent and distributed systems by restricted timed automata....Pages 169-183
Transformational formal development of real-time systems....Pages 184-198
A transformation of monitor into communication synchronized parallel processes: A systematic refinement step in design....Pages 199-215
Contracts for ODP....Pages 216-232
Affine transformations in Signal and their application in the specification and validation of real-time systems....Pages 233-247
Action-based concurrency and synchronization for objects....Pages 248-262
Communication Extended Abstract Types in the refinement of parallel communicating processes....Pages 263-279
Verification and refinement of distributed programs in a fair framework....Pages 280-294
Formalizing real-time scheduling as program refinement....Pages 295-309
Specification and refinement of continuous real-time systems....Pages 310-324
High-level execution time analysis....Pages 325-339
A sound and complete proof system for probabilistic processes....Pages 340-352
Testing semantics for a probabilistic-timed process algebra....Pages 353-367
Denotational semantics for timed testing....Pages 368-382
Extending LOTOS with time: A true concurrency perspective....Pages 383-399
Introduction of a suspend/resume operator in ET-LOTOS....Pages 400-414
Specification and verification of a real-time field bus with formal description languages....Pages 415-429