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

• Συγγραφή απο Οργανισμό/Αρχή: 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
• Θέματα: Computers.; Software engineering.; Computer logic.; Programming languages (Electronic computers).; Special purpose computers.; Theory of Computation.; Software Engineering/Programming and Operating Systems.; Logics and Meanings of Programs.; Software Engineering.; Programming Languages, Compilers, Interpreters.; Special Purpose and Application-Based Systems.

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....

Πίνακας περιεχομένων:

• 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%.