Ebook: Formal Description Techniques and Protocol Specification, Testing and Verification: FORTE X / PSTV XVII ’97

FORTE/PSTV '97 addresses Formal Description Techniques (FDTs) applicable to Distributed Systems and Communication Protocols (such as Estelle, LOTOS, SDL, ASN.1, TTCN, Z, Automata, Process Algebra, Logic). The conference is a forum for presentation of the state-of-the-art in theory, application, tools and industrialization of FDTs, and provides an excellent orientation for newcomers.

---

---

Content:
Front Matter....Pages i-xi
Front Matter....Pages 1-1
Specification-based testing of concurrent systems....Pages 7-22
Refusal testing for classes of transition systems with inputs and outputs....Pages 23-39
A Framework for Distributed Object-Oriented Testing....Pages 39-56
Interoperability Test Suite Derivation for Symmetric Communication Protocols....Pages 57-72
A Hierarchy of Communication Models for Message Sequence Charts....Pages 75-90
Timing Constraints in Message Sequence Chart Specifications....Pages 91-106
Consistent Semantics for ODP Information and Computational Models....Pages 107-126
Specifying the ODP Trader: An Introduction to E-LOTOS....Pages 127-142
A Computer Aided Design of a Secure Registration Protocol....Pages 145-160
Implementation of Distributed Systems described with LOTOS Multi-rendezvous on Bus Topology Networks....Pages 161-176
Disjunction of LOTOS specifications....Pages 177-192
A timed automaton model for ET-LOTOS verification....Pages 193-204
Automatic Checking of Aggregation Abstractions Through State Enumeration....Pages 207-222
Concept of Quantified Abstract Quotient Automaton and its advantage....Pages 223-238
Validating Protocol Composition for Progress by Parallel Step Reachability Analysis....Pages 239-250
An Improved Search Strategy for Lossy Channel Systems....Pages 251-264
A weighted random walk approach for conformance testing of a system specified as communicating finite state machines....Pages 267-282
Friendly Testing as a Conformance Relation....Pages 283-298
Generalized metric based test selection and coverage measure for communication protocols....Pages 299-314
Front Matter....Pages 315-315
Dynamic priorities for modeling real-time....Pages 321-336
Front Matter....Pages 315-315
On-line timed protocol trace analysis based on uncertain state descriptions....Pages 337-352
Algebraic Specification through Expression Transformation....Pages 355-366
Modelling Digital Logic in SDL....Pages 367-382
A Methodology for the Description of System Requirements and the Derivation of Formal Specifications....Pages 383-398
On the Influence of Semantic Constraints on the Code Generation from Estelle Specifications....Pages 399-414
Using a Formal Description Technique to Model Aspects of a Global Air Traffic Telecommunications Network....Pages 417-432
An experiment in using RT-LOTOS for the formal specification and verification of a distributed scheduling algorithm in a nuclear power plant monitoring system....Pages 433-448
Intelligent Protocol Analyzer with TCP Behavior Emulation for Interoperability Testing of TCP/IP Protocols....Pages 449-464
Eight years of experience in test generation from FDTs using TVEDA....Pages 465-480
Front Matter....Pages 481-481
Self-independent Petri Nets for Distributed Systems....Pages 487-502
Combining CSP and Object-Z: Finite or Infinite Trace Semantics?....Pages 503-518
Selective mu-calculus: New Modal Operators for Proving Properties on Reduced Transition Systems....Pages 519-534
On a Concurrency Calculus for Design of Mobile Telecommunication Systems....Pages 535-546
Back Matter....Pages 547-550

---

Content:
Front Matter....Pages i-xi
Front Matter....Pages 1-1
Specification-based testing of concurrent systems....Pages 7-22
Refusal testing for classes of transition systems with inputs and outputs....Pages 23-39
A Framework for Distributed Object-Oriented Testing....Pages 39-56
Interoperability Test Suite Derivation for Symmetric Communication Protocols....Pages 57-72
A Hierarchy of Communication Models for Message Sequence Charts....Pages 75-90
Timing Constraints in Message Sequence Chart Specifications....Pages 91-106
Consistent Semantics for ODP Information and Computational Models....Pages 107-126
Specifying the ODP Trader: An Introduction to E-LOTOS....Pages 127-142
A Computer Aided Design of a Secure Registration Protocol....Pages 145-160
Implementation of Distributed Systems described with LOTOS Multi-rendezvous on Bus Topology Networks....Pages 161-176
Disjunction of LOTOS specifications....Pages 177-192
A timed automaton model for ET-LOTOS verification....Pages 193-204
Automatic Checking of Aggregation Abstractions Through State Enumeration....Pages 207-222
Concept of Quantified Abstract Quotient Automaton and its advantage....Pages 223-238
Validating Protocol Composition for Progress by Parallel Step Reachability Analysis....Pages 239-250
An Improved Search Strategy for Lossy Channel Systems....Pages 251-264
A weighted random walk approach for conformance testing of a system specified as communicating finite state machines....Pages 267-282
Friendly Testing as a Conformance Relation....Pages 283-298
Generalized metric based test selection and coverage measure for communication protocols....Pages 299-314
Front Matter....Pages 315-315
Dynamic priorities for modeling real-time....Pages 321-336
Front Matter....Pages 315-315
On-line timed protocol trace analysis based on uncertain state descriptions....Pages 337-352
Algebraic Specification through Expression Transformation....Pages 355-366
Modelling Digital Logic in SDL....Pages 367-382
A Methodology for the Description of System Requirements and the Derivation of Formal Specifications....Pages 383-398
On the Influence of Semantic Constraints on the Code Generation from Estelle Specifications....Pages 399-414
Using a Formal Description Technique to Model Aspects of a Global Air Traffic Telecommunications Network....Pages 417-432
An experiment in using RT-LOTOS for the formal specification and verification of a distributed scheduling algorithm in a nuclear power plant monitoring system....Pages 433-448
Intelligent Protocol Analyzer with TCP Behavior Emulation for Interoperability Testing of TCP/IP Protocols....Pages 449-464
Eight years of experience in test generation from FDTs using TVEDA....Pages 465-480
Front Matter....Pages 481-481
Self-independent Petri Nets for Distributed Systems....Pages 487-502
Combining CSP and Object-Z: Finite or Infinite Trace Semantics?....Pages 503-518
Selective mu-calculus: New Modal Operators for Proving Properties on Reduced Transition Systems....Pages 519-534
On a Concurrency Calculus for Design of Mobile Telecommunication Systems....Pages 535-546
Back Matter....Pages 547-550
....