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....
Συγγραφή απο Οργανισμό/Αρχή: | |
---|---|
Άλλοι συγγραφείς: | , , |
Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
Γλώσσα: | 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%.