FM'99 - Formal Methods World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999 Proceedings, Volume II /

Formal methods are coming of age. Mathematical techniques and tools are now regarded as an important part of the development process in a wide range of industrial and governmental organisations. A transfer of technology into the mainstream of systems development is slowly, but surely, taking place....

Πλήρης περιγραφή

Λεπτομέρειες βιβλιογραφικής εγγραφής
Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
Άλλοι συγγραφείς: Wing, Jeannette M. (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Woodcook, Jim (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Davies, Jim (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
Γλώσσα:English
Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1999.
Έκδοση:1st ed. 1999.
Σειρά:Lecture Notes in Computer Science, 1709
Θέματα:
Διαθέσιμο Online:Full Text via HEAL-Link
Πίνακας περιεχομένων:
  • Foundations of System Specification (IFIP WG 1.3)
  • From informal requirements to COOP: a concurrent automata approach
  • A framework for defining Object-Calculi extended abstract
  • European Theory and Practice of Software (ETAPS)
  • A translation of statecharts to esterel
  • An operational semantics for timed RAISE
  • Data abstraction for CSP-OZ
  • Systems development using Z generics
  • A brief summary of VSPEC
  • Enhancing the pre- and postcondition technique for more expressive specifications
  • Program Verification
  • On excusable and inexcusable failures towards an adequate notion of translation correctness
  • Interfacing program construction and verification
  • Software verification based on linear programming
  • Integration of Notation and Techniques
  • Sensors and actuators in TCOZ
  • The UniForM workbench a universal development environment for formal methods
  • Integrating formal description techniques
  • Formal Description of Programming Concepts (IFIP WG 2.2)
  • A more complete TLA
  • Formal justification of the rely-guarantee paradigm for shared-variable concurrency: a semantic approach
  • Relating Z and first-order logic
  • Open Information Systems
  • Formal modeling of the enterprise javabeans™ component integration framework
  • Developing components in the presence of re-entrance
  • Communication and synchronisation using interaction objects
  • Modelling microsoft COM using ?-calculus
  • Co-design
  • Validation of mixed signal-alpha real-time systems through affine calculus on clock synchronisation constraints
  • Combining theorem proving and continuous models in synchronous design
  • Parts a partitioning transformation system
  • A behavioral model for co-design
  • Refinement
  • A weakest precondition semantics for an object-oriented language of refinement
  • Reasoning about interactive systems
  • Non-atomic refinement in Z
  • Refinement semantics and loop rules
  • Safety
  • Lessons from the application of formal methods to the design of a storm surge barrier control system
  • The value of verification: positive experience of Industrial proof
  • Formal development and verification of a distributed railway control system
  • Safety analysis in formal specication
  • Formal specification and validation of a vital communication protocol
  • Incremental design of a Power transformer station controller using a controller synthesis methodology
  • OBJ/Cafe OBJ/Maude
  • Verifying behavioural specifications in CafeOBJ environment
  • Component-based algebraic specification and verification in cafeOBJ
  • Using algebraic specification techniques in development of object-oriented frameworks
  • Maude as a formal meta-tool
  • Hiding more of hidden algebra
  • Abstract State Machines (ASM) and Algebraic Methods in Software Technology (AMAST)
  • A termination detection algorithm: specification and verification
  • Logspace reducibility via abstract state machines
  • Formal methods for extensions to CAS
  • An lgebraic framework for higher-order odules
  • Avionics
  • Applying formal proof techniques to avionics software: a pragmatic approach
  • Secure synthesis of code: a process improvement experiment
  • Cronos: a separate compilation tool set for modular esterel applications
  • Works-in-Progress
  • Tool support for production use of formal techniques
  • Modeling aircraft mission computer task rates
  • A study of collaborative work: answers to a test on formal specification in B
  • Archived design steps in temporal logic
  • A PVS-based approach for teaching constructing correct iterations
  • A minimal framework for specification theory
  • A model of specification-based testing of interactive systems
  • Algebraic aspects of the mapping between abstract syntax notation one and CORBA IDL
  • Retrenchment
  • Proof preservation in component generalization
  • Industrial Experience
  • Formal modelling and simulation of train control systems using petri nets
  • Formal specification of a voice communication system used in air traffic control an industrial application of light-weight formal methods using vdm
  • Model-checking the architectural design of a fail-safe communication system for railway interlocking systems
  • Analyzing the requirements of an access control using VDMTools and PVS
  • Cache coherence verification with TLA%.