Formal Description Techniques IX: Theory, application and tools

Front Matter....Pages i-x
Front Matter....Pages 1-1
The Video Dial Tone Service and the ATM Environment....Pages 3-25
Front Matter....Pages 27-27
Computer-Assisted Verification of an Algorithm for Concurrent Timestamps....Pages 29-44
Design and Optimization of High-Performance Protocols with the DO-IT Toolbox....Pages 45-60
Tool support for algebraic specifications of data in SDL-92....Pages 61-76
Automating Performance Optimisation by Heuristic Analysis of A Formal Specification....Pages 77-92
Front Matter....Pages 93-93
Formal description techniques - how formal and descriptive are they?....Pages 95-110
Front Matter....Pages 111-111
Using Formal Methods in the Development of Protocols for Multi-User Multimedia Systems....Pages 113-128
Formal Verification of Communication Protocols....Pages 129-144
Applications of Fair Testing....Pages 145-160
Front Matter....Pages 161-161
Fault models for testing in context....Pages 163-178
EPER: Efficient Packed Encoding Rules for ASN.1....Pages 179-194
Relating conformance test coverage to formal specifications....Pages 195-210
Front Matter....Pages 211-211
Performance Modelling with the Formal Specification Language SDL....Pages 213-228
The QUEST-Approach for the Performance Evaluation of SDL-Systems....Pages 229-244
A Formal Description Language for the Modelling and Simulation of Timed Interaction Diagrams....Pages 245-260
Front Matter....Pages 261-261
Model Reduction of Modules for State-Event Temporal Logics....Pages 263-278
Time-Action Alternating Model for Timed LOTOS and its Symbolic Verification of Bisimulation Equivalence....Pages 279-294
A Timed Semantics for SDL....Pages 295-309
Implementation of multimedia systems based on a real-time extension of Estelle....Pages 310-326
Front Matter....Pages 327-327
Using Formal Methods: if you’re so smart how come you ain’t rich?....Pages 329-329
Front Matter....Pages 331-331
A New Scheme for Memory-Efficient Probabilistic Verification....Pages 333-348
Direct Verification of Bisimulations....Pages 349-363
Finitely Representing Infinite Reachability Graphs of CFSMs with Graph Grammars....Pages 364-379
Model Checking Based on Occurrence Net Graph....Pages 380-395
Front Matter....Pages 397-397
Network Computing....Pages 399-399
Front Matter....Pages 401-401
Validation-Based Test Sequence Generation for Networks of Extended Finite State Machines....Pages 403-418
Using SDL for the specification, simulation and implementation of an advanced OSI data—link protocol on an embedded microcontroller system....Pages 419-434
Specification and Verification of the PowerScaleTM Bus Arbitration Protocol: An Industrial Experiment with LOTOS....Pages 435-450
Combined Application of SDL-92, OMT, MSC and TTCN....Pages 451-466
Front Matter....Pages 467-467
On the Introduction of Exceptions in E-LOTOS....Pages 469-484
From LOTOS to Petri Nets through Iexpansion....Pages 485-500
Comparing LOTOS and Z refinement relations....Pages 501-516
Back Matter....Pages 517-518