LEADER 06855nam 22007575 450 001 996466079203316 005 20220920150435.0 010 $a3-540-47623-7 024 7 $a10.1007/BFb0024633 035 $a(CKB)1000000000233954 035 $a(SSID)ssj0000323188 035 $a(PQKBManifestationID)11223082 035 $a(PQKBTitleCode)TC0000323188 035 $a(PQKBWorkID)10296778 035 $a(PQKB)10257824 035 $a(DE-He213)978-3-540-47623-8 035 $a(PPN)155219553 035 $a(EXLCZ)991000000000233954 100 $a20121227d1993 u| 0 101 0 $aeng 135 $aurnn#--8mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aFME '93: Industrial-Strength Formal Methods$b[electronic resource] $eFirst International Symposium of Formal Methods Europe, Odense, Denmark, April 19-23, 1993. Proceedings /$fedited by James C.P. Woodcock, Peter G. Larsen 205 $a1st ed. 1993. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1993. 215 $a1 online resource (XIII, 695 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v670 300 $aBibliographic Level Mode of Issuance: Monograph 311 1 $a3-540-56662-7 327 $aReasoning about interference in an object-based design method -- Using relative refinement for fault tolerance -- Specification and validation of a security policy model -- Experiences from applications of RAISE -- Role of VDM(++) in the development of a real-time tracking and tracing system -- The integration of LOTOS with an object oriented development method -- An industrial experience on LOTOS-based prototyping for switching systems design -- Towards an implementation-oriented specification of TP protocol in LOTOS -- A metalanguage for the formal requirement specification of reactive systems -- Model checking in practice -- Algorithm refinement with read and write frames -- Invariants, frames and postconditions: a comparison of the VDM and B notations -- The industrial take-up of formal methods in safety-critical and other areas: A perspective -- A proof environment for concurrent programs -- A VDM ? study of Fault-Tolerant stable storage ? Towards a computer engineering mathematics -- Applications of modal logic for the specification of real-time systems -- Formal methods reality check: Industrial usage -- Automating the generation and sequencing of test cases from model-based specifications -- The parallel abstract machine: A common execution model for FDTs -- Generalizing Abadi & Lamport's method to solve a problem posed by A. Pnueli -- Real-time refinement -- Different FDT's confronted with different ODP-viewpoints of the trader -- On the derivation of executable database programs from formal specifications -- A concurrency case study using RAISE -- Specifying a safety-critical control system in Z -- An overview of the SPRINT method -- Application of composition development method for definition of SYNTHESIS information resource query language semantics -- Verification tools in the development of provably correct compilers -- Encoding W : A Logic for Z in 2OBJ -- Formal verification for fault-tolerant architectures: Some lessons learned -- Conformity clause for VDM-SL -- Process instances in LOTOS simulation -- The SAZ project: Integrating SSADM and Z -- Maintaining consistency under changes to formal specifications -- An EVES data abstraction example -- Putting advanced reachability analysis techniques together: The ?ARA? tool -- Integrating SA/RT with LOTOS -- Symbolic model checking for distributed real-time systems -- Adding specification constructors to the refinement calculus -- Selling formal methods to industry -- Tool Descriptions. 330 $aThe last few years have borne witness to a remarkable diversity of formal methods, with applications to sequential and concurrent software, to real-time and reactive systems, and to hardware design. In that time, many theoretical problems have been tackled and solved, and many continue to be worked upon. Yet it is by the suitability of their industrial application and the extent of their usage that formal methods will ultimately be judged. This volume presents the proceedings of the first international symposium of Formal Methods Europe, FME'93. The symposium focuses on the application of industrial-strength formal methods. Authors address the difficulties of scaling their techniques up to industrial-sized problems, and their suitability in the workplace, and discuss techniques that are formal (that is, they have a mathematical basis) and that are industrially applicable. The volume has four parts: - Invited lectures, containing a lecture by Cliff B. Jones and a lecture by Antonio Cau and Willem-Paul de Roever; - Industrial usage reports, containing 6 reports; - Papers, containing 32 selected and refereedpapers; - Tool descriptions, containing 11 descriptions. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v670 606 $aSoftware engineering 606 $aApplication software 606 $aComputer programming 606 $aComputer logic 606 $aInformation technology 606 $aBusiness?Data processing 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 606 $aComputer Applications$3https://scigraph.springernature.com/ontologies/product-market-codes/I23001 606 $aProgramming Techniques$3https://scigraph.springernature.com/ontologies/product-market-codes/I14010 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aIT in Business$3https://scigraph.springernature.com/ontologies/product-market-codes/522000 615 0$aSoftware engineering. 615 0$aApplication software. 615 0$aComputer programming. 615 0$aComputer logic. 615 0$aInformation technology. 615 0$aBusiness?Data processing. 615 14$aSoftware Engineering/Programming and Operating Systems. 615 24$aComputer Applications. 615 24$aProgramming Techniques. 615 24$aSoftware Engineering. 615 24$aLogics and Meanings of Programs. 615 24$aIT in Business. 676 $a005.13/1 702 $aWoodcock$b James C.P$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aLarsen$b Peter G$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aInternational Symposium of Formal Methods Europe 906 $aBOOK 912 $a996466079203316 996 $aFME '93: Industrial-Strength Formal Methods$92831381 997 $aUNISA