FME '94: Industrial Benefit of Formal Methods [[electronic resource] ] : Second International Symposium of Formal Methods Europe, Barcelona, Spain, October 24 - 28, 1994. Proceedings / / edited by Maurice Naftalin, Tim Denvir, Miquel Bertran |
Edizione | [1st ed. 1994.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1994 |
Descrizione fisica | 1 online resource (XII, 732 p.) |
Disciplina | 005.1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Application software Computer programming Programming languages (Electronic computers) Computer logic Software Engineering/Programming and Operating Systems Computer Applications Programming Techniques Software Engineering Programming Languages, Compilers, Interpreters Logics and Meanings of Programs |
ISBN | 3-540-49031-0 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | From action systems to modular systems -- Formal methods in the railways signalling industry -- Formal and informal specifications of a secure system component: first results in a comparative study -- Formalising British rail's signalling rules -- Three applications of formal methods at MITRE -- Specification and analysis of a security management system -- Verification techniques for LOTOS -- Experiences in using the abstract machine notation in a GKS case study -- Seven more myths of formal methods: Dispelling industrial prejudices -- Comparing approaches to data reification -- Towards a formalization of programming-by-difference -- A new concept of refinement used for behaviour modelling with automata -- An extended VDM refinement relation -- On transferring VDM verification techniques to Z -- Proof-based development of specifications with KIDS/VDM -- Evaluation of underdetermined explicit definitions -- A precise examination of the behaviour of process models -- A theory of presentations -- Applying a concurrent formal framework to process modelling -- From MooZ to eiffel — A rigorous approach to system development -- OPUS: a formal approach to object-orientation -- A strategy for the production of verifiable code using the B Method -- Specifying & verifying concurrent systems using Z -- A critical look at functional specifications -- Informal strategies in design by refinement -- An experimental support system for formal mathematical reasoning -- Literate mathematical development of a revision management system -- An action semantics for ML concurrency primitives -- A semantics for NewSpeak in VDM-SL -- Evaluation semantics in Z -- Abstract model checking of infinite specifications -- Case study: Specification and refinement of the PI-Bus -- Stepwise refinement of control software — A case study using RAISE -- Specifying safety and progress properties with RSL -- Validation of a railway interlocking model -- A formal specification of an automatic train protection system -- Adding real time to formal program development -- Combining the design of industrial systems with effective verification techniques -- RTL and refutation by positive cycles -- Formalising the semantics of Ward/Mellor SA/RT essential models using a process algebra -- Deriving relational database programs from formal specifications. |
Record Nr. | UNISA-996466093103316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1994 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Transformation-based reactive systems development : 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS'97, Palma, Mallorca, Spain, May 21-23, 1997 ; proceedings / / Miquel Bertran, Teodor Rus, eds |
Edizione | [1st ed. 1997.] |
Pubbl/distr/stampa | Berlin, Germany ; ; New York, New York : , : Springer, , [1997] |
Descrizione fisica | 1 online resource (XI, 436 p.) |
Disciplina | 005.2/73 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Electronic data processing - Distributed processing
Real-time data processing Parallel processing (Electronic computers) |
ISBN | 3-540-69058-1 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | What was Llull up to? -- Llull as computer scientist or why Llull was one of us -- Deductive verification of real-time systems using STeP -- Refinement of Time -- The verus language: Representing time efficiently with BDDs -- Refining interval temporal logic specifications -- Integrating temporal logics and model checking algorithms -- PLC-automata: A new class of implementable real-time automata -- Communication concepts for statecharts: A semantic foundation -- Regular processes and timed automata -- A visual formalism for real time requirement specifications -- Formal specification and verification method of concurrent and distributed systems by restricted timed automata -- Transformational formal development of real-time systems -- A transformation of monitor into communication synchronized parallel processes: A systematic refinement step in design -- Contracts for ODP -- Affine transformations in Signal and their application in the specification and validation of real-time systems -- Action-based concurrency and synchronization for objects -- Communication Extended Abstract Types in the refinement of parallel communicating processes -- Verification and refinement of distributed programs in a fair framework -- Formalizing real-time scheduling as program refinement -- Specification and refinement of continuous real-time systems -- High-level execution time analysis -- A sound and complete proof system for probabilistic processes -- Testing semantics for a probabilistic-timed process algebra -- Denotational semantics for timed testing -- Extending LOTOS with time: A true concurrency perspective -- of a suspend/resume operator in ET-LOTOS -- Specification and verification of a real-time field bus with formal description languages. |
Record Nr. | UNINA-9910144922103321 |
Berlin, Germany ; ; New York, New York : , : Springer, , [1997] | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Transformation-based reactive systems development : 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS'97, Palma, Mallorca, Spain, May 21-23, 1997 ; proceedings / / Miquel Bertran, Teodor Rus, eds |
Edizione | [1st ed. 1997.] |
Pubbl/distr/stampa | Berlin, Germany ; ; New York, New York : , : Springer, , [1997] |
Descrizione fisica | 1 online resource (XI, 436 p.) |
Disciplina | 005.2/73 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Electronic data processing - Distributed processing
Real-time data processing Parallel processing (Electronic computers) |
ISBN | 3-540-69058-1 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | What was Llull up to? -- Llull as computer scientist or why Llull was one of us -- Deductive verification of real-time systems using STeP -- Refinement of Time -- The verus language: Representing time efficiently with BDDs -- Refining interval temporal logic specifications -- Integrating temporal logics and model checking algorithms -- PLC-automata: A new class of implementable real-time automata -- Communication concepts for statecharts: A semantic foundation -- Regular processes and timed automata -- A visual formalism for real time requirement specifications -- Formal specification and verification method of concurrent and distributed systems by restricted timed automata -- Transformational formal development of real-time systems -- A transformation of monitor into communication synchronized parallel processes: A systematic refinement step in design -- Contracts for ODP -- Affine transformations in Signal and their application in the specification and validation of real-time systems -- Action-based concurrency and synchronization for objects -- Communication Extended Abstract Types in the refinement of parallel communicating processes -- Verification and refinement of distributed programs in a fair framework -- Formalizing real-time scheduling as program refinement -- Specification and refinement of continuous real-time systems -- High-level execution time analysis -- A sound and complete proof system for probabilistic processes -- Testing semantics for a probabilistic-timed process algebra -- Denotational semantics for timed testing -- Extending LOTOS with time: A true concurrency perspective -- of a suspend/resume operator in ET-LOTOS -- Specification and verification of a real-time field bus with formal description languages. |
Record Nr. | UNISA-996465541303316 |
Berlin, Germany ; ; New York, New York : , : Springer, , [1997] | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|