Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Dependable software engineering : theories, tools, and applications : 7th International Symposium, SETTA 2021, Beijing, China, November 25-27, 2021, proceedings / / Shengchao Qin, Jim Woodcock, Wenhui Zhang (editors)
| Dependable software engineering : theories, tools, and applications : 7th International Symposium, SETTA 2021, Beijing, China, November 25-27, 2021, proceedings / / Shengchao Qin, Jim Woodcock, Wenhui Zhang (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (327 pages) |
| Disciplina | 005.1 |
| Collana | Lecture notes in computer science, programming and software engineering |
| Soggetto topico |
Software engineering
Formal methods (Computer science) |
| ISBN | 3-030-91265-5 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910510561103321 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Dependable software engineering : theories, tools, and applications : 7th International Symposium, SETTA 2021, Beijing, China, November 25-27, 2021, proceedings / / Shengchao Qin, Jim Woodcock, Wenhui Zhang (editors)
| Dependable software engineering : theories, tools, and applications : 7th International Symposium, SETTA 2021, Beijing, China, November 25-27, 2021, proceedings / / Shengchao Qin, Jim Woodcock, Wenhui Zhang (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (327 pages) |
| Disciplina | 005.1 |
| Collana | Lecture notes in computer science, programming and software engineering |
| Soggetto topico |
Software engineering
Formal methods (Computer science) |
| ISBN | 3-030-91265-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996464526803316 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Domain Modeling and the Duration Calculus : International Training School, Shanghai, China, September 17-21, 2007, Advanced Lectures / / edited by Chris George, Zhiming Liu, Jim Woodcock
| Domain Modeling and the Duration Calculus : International Training School, Shanghai, China, September 17-21, 2007, Advanced Lectures / / edited by Chris George, Zhiming Liu, Jim Woodcock |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (XI, 240 p.) |
| Disciplina | 004.33 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Computer systems Computer science Computer networks Algorithms Software Engineering Computer System Implementation Computer Science Logic and Foundations of Programming Computer Communication Networks |
| ISBN | 3-540-74964-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Delivering Real-Time Behaviour -- Applicative Modelling with RAISE -- A Theory of Duration Calculus with Application -- Understanding Programming Language Concepts Via Operational Semantics. |
| Record Nr. | UNINA-9910485022703321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Domain Modeling and the Duration Calculus : International Training School, Shanghai, China, September 17-21, 2007, Advanced Lectures / / edited by Chris George, Zhiming Liu, Jim Woodcock
| Domain Modeling and the Duration Calculus : International Training School, Shanghai, China, September 17-21, 2007, Advanced Lectures / / edited by Chris George, Zhiming Liu, Jim Woodcock |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (XI, 240 p.) |
| Disciplina | 004.33 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Computer systems Computer science Computer networks Algorithms Software Engineering Computer System Implementation Computer Science Logic and Foundations of Programming Computer Communication Networks |
| ISBN | 3-540-74964-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Delivering Real-Time Behaviour -- Applicative Modelling with RAISE -- A Theory of Duration Calculus with Application -- Understanding Programming Language Concepts Via Operational Semantics. |
| Record Nr. | UNISA-996466093703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Fm'99--formal methods : world congress on formal methods in the development of computing systems, Toulouse, france, September 20-24, 1999 : proceedings / / edited by Jeannette M. Wing, Jim Woodcock, Jim Davies
| Fm'99--formal methods : world congress on formal methods in the development of computing systems, Toulouse, france, September 20-24, 1999 : proceedings / / edited by Jeannette M. Wing, Jim Woodcock, Jim Davies |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (XXXVI, 940 p.) |
| Disciplina | 005.131 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Application software - Development
Formal methods (Computer science) |
| ISBN | 3-540-48119-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle -- Scientific Decisions which Characterize VDM -- Mechanized Formal Methods: Where Next? -- Integration, the Price of Success -- The Role of Formalism in Method -- Integration into the Development Process -- Formal Design for Automatic Coding and Testing: The ESSI/SPACES Project -- A Business Process Design Language -- Software Architecture -- Refinement of Pipe-and-Filter Architectures -- A Formalization of Software Architecture -- European Association for Theoretical Computer Science (EATCS) -- Component and Interface Refinement in Closed-System Specifications -- Semantics of First Order Parametric Specifications -- Model Checking -- A Perfecto Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software -- Error Detection with Directed Symbolic Model Checking -- Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination -- On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems -- On-the-fly Verification of Linear Temporal Logic -- Symbolic Model Checking with Fewer Fixpoint Computations -- Formula Based Abstractions of Transition Systems for Real-Time Model Checking -- If: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems -- Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes -- The B Method -- The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications -- Météor: A Successful Application of B in a Large Project -- Formal Development of Databases in ASSO and B -- Interpreting the B-Method in the Refinement Calculus -- Compositional Symmetric Sharing in B -- Structural Embeddings: Mechanization with Method -- The Safe Machine: A New Specification Construct for B -- csp2B: A Practical Approach to Combining CSP and B -- Test Criteria Definition for B Models -- Composition and Synthesis -- Bunches for Object-Oriented, Concurrent, and Real-Time Specification -- Applications of Structural Synthesis of Programs -- Towards a Compositional Approach to the Design and Verification of Distributed Systems -- Telecommunications -- Formal Modeling in a Commercial Setting: A Case Study -- KVEST: Automated Generation of Test Suites from Formal Specifications -- Feature Interaction Detection Using Testing and Model-Checking Experience Report -- Emma: Developing an Industrial Reachability Analyser for SDL -- Correctness Proof of the Standardized Algorithm for ABR Conformance -- Verifying a Distributed Database Lookup Manager Written in Erlang -- Security -- Secure Interoperation of Secure Distributed Databases -- A Formal Security Model for Microprocessor Hardware -- Abstraction and Testing -- Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol -- Probabilistic Polynomial-Time Equivalence and Security Analysis -- A Uniform Approach for the Definition of Security Properties -- Group Principals and the Formalization of Anonymity -- Object-Orientation -- Developing BON as an Industrial-Strength Formal Method -- On the Expressive Power of OCL -- A Systematic Approach to Transform OMT Diagrams to a B Specification -- Verifying Consistency and Validity of Formal -- Verifying Consistency and Validity of Formal Specifications by Testing -- A GSM-MAP Protocol Experiment Using Passive Testing. |
| Altri titoli varianti | Formal methods |
| Record Nr. | UNISA-996465302703316 |
| Berlin : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Fm'99--formal methods . Volume ii : world congress on formal methods in the development of computing systems, toulouse, france, september 20-24, 1999 proceedings / / edited by Jeannette M. Wing, Jim Woodcock, Jim Davies
| Fm'99--formal methods . Volume ii : world congress on formal methods in the development of computing systems, toulouse, france, september 20-24, 1999 proceedings / / edited by Jeannette M. Wing, Jim Woodcock, Jim Davies |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin, Germany ; ; New York, New York : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (XVIII, 942 p.) |
| Disciplina | 005.131 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Application software - Development
Formal methods (Computer science) |
| ISBN | 3-540-48118-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 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%. |
| Altri titoli varianti | Formal methods |
| Record Nr. | UNISA-996465304103316 |
| Berlin, Germany ; ; New York, New York : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Fm'99--formal methods : world congress on formal methods in the development of computing systems, Toulouse, france, September 20-24, 1999 : proceedings / / edited by Jeannette M. Wing, Jim Woodcock, Jim Davies
| Fm'99--formal methods : world congress on formal methods in the development of computing systems, Toulouse, france, September 20-24, 1999 : proceedings / / edited by Jeannette M. Wing, Jim Woodcock, Jim Davies |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (XXXVI, 940 p.) |
| Disciplina | 005.131 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Application software - Development
Formal methods (Computer science) |
| ISBN | 3-540-48119-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle -- Scientific Decisions which Characterize VDM -- Mechanized Formal Methods: Where Next? -- Integration, the Price of Success -- The Role of Formalism in Method -- Integration into the Development Process -- Formal Design for Automatic Coding and Testing: The ESSI/SPACES Project -- A Business Process Design Language -- Software Architecture -- Refinement of Pipe-and-Filter Architectures -- A Formalization of Software Architecture -- European Association for Theoretical Computer Science (EATCS) -- Component and Interface Refinement in Closed-System Specifications -- Semantics of First Order Parametric Specifications -- Model Checking -- A Perfecto Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software -- Error Detection with Directed Symbolic Model Checking -- Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination -- On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems -- On-the-fly Verification of Linear Temporal Logic -- Symbolic Model Checking with Fewer Fixpoint Computations -- Formula Based Abstractions of Transition Systems for Real-Time Model Checking -- If: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems -- Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes -- The B Method -- The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications -- Météor: A Successful Application of B in a Large Project -- Formal Development of Databases in ASSO and B -- Interpreting the B-Method in the Refinement Calculus -- Compositional Symmetric Sharing in B -- Structural Embeddings: Mechanization with Method -- The Safe Machine: A New Specification Construct for B -- csp2B: A Practical Approach to Combining CSP and B -- Test Criteria Definition for B Models -- Composition and Synthesis -- Bunches for Object-Oriented, Concurrent, and Real-Time Specification -- Applications of Structural Synthesis of Programs -- Towards a Compositional Approach to the Design and Verification of Distributed Systems -- Telecommunications -- Formal Modeling in a Commercial Setting: A Case Study -- KVEST: Automated Generation of Test Suites from Formal Specifications -- Feature Interaction Detection Using Testing and Model-Checking Experience Report -- Emma: Developing an Industrial Reachability Analyser for SDL -- Correctness Proof of the Standardized Algorithm for ABR Conformance -- Verifying a Distributed Database Lookup Manager Written in Erlang -- Security -- Secure Interoperation of Secure Distributed Databases -- A Formal Security Model for Microprocessor Hardware -- Abstraction and Testing -- Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol -- Probabilistic Polynomial-Time Equivalence and Security Analysis -- A Uniform Approach for the Definition of Security Properties -- Group Principals and the Formalization of Anonymity -- Object-Orientation -- Developing BON as an Industrial-Strength Formal Method -- On the Expressive Power of OCL -- A Systematic Approach to Transform OMT Diagrams to a B Specification -- Verifying Consistency and Validity of Formal -- Verifying Consistency and Validity of Formal Specifications by Testing -- A GSM-MAP Protocol Experiment Using Passive Testing. |
| Altri titoli varianti | Formal methods |
| Record Nr. | UNINA-9910767573803321 |
| Berlin : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Fm'99--formal methods . Volume ii : world congress on formal methods in the development of computing systems, toulouse, france, september 20-24, 1999 proceedings / / edited by Jeannette M. Wing, Jim Woodcock, Jim Davies
| Fm'99--formal methods . Volume ii : world congress on formal methods in the development of computing systems, toulouse, france, september 20-24, 1999 proceedings / / edited by Jeannette M. Wing, Jim Woodcock, Jim Davies |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin, Germany ; ; New York, New York : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (XVIII, 942 p.) |
| Disciplina | 005.131 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Application software - Development
Formal methods (Computer science) |
| ISBN | 3-540-48118-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 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%. |
| Altri titoli varianti | Formal methods |
| Record Nr. | UNINA-9910767573303321 |
| Berlin, Germany ; ; New York, New York : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods : foundations and applications ; 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009 ; revised selected papers / / Marcel Vinicius Medeiros Oliveira, Jim Woodcock (eds.)
| Formal methods : foundations and applications ; 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009 ; revised selected papers / / Marcel Vinicius Medeiros Oliveira, Jim Woodcock (eds.) |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | New York ; ; Berlin, : Springer, c2009 |
| Descrizione fisica | 1 online resource (X, 351 p.) |
| Disciplina | 004 |
| Altri autori (Persone) |
OliveiraMarcel Vinicius Medeiros
WoodcockJim |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Formal methods (Computer science)
Electronic data processing |
| ISBN | 3-642-10452-5 |
| Classificazione |
DAT 310f
DAT 325f SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Speeding Up Simulation of SystemC Using Model Checking -- Partial Behaviour Modelling: Foundations for Incremental and Iterative Model-Based Software Engineering -- Satisfiability Modulo Theories: An Appetizer -- Interruption Testing of Reactive Systems -- Test Case Generation of Embedded Real-Time Systems with Interruptions for FreeRTOS -- Concurrent Models of Flash Memory Device Behaviour -- Corecursive Algebras: A Study of General Structured Corecursion -- Formalizing FreeRTOS: First Steps -- A Mechanized Strategy for Safe Abstraction of CSP Specifications -- Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B -- An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model -- Towards Safe Design of Synchronous Bus Protocols in Event-B -- Mechanising Data-Types for Kernel Design in Z -- A Complete Set of Object Modeling Laws for Alloy -- Undecidability Results for Distributed Probabilistic Systems -- Formalisation and Analysis of Objects as CSP Processes -- Concolic Testing of the Multi-sector Read Operation for Flash Memory File System -- Low-Level Code Verification Based on CSP Models -- Formal Modelling of a Microcontroller Instruction Set in B -- Defining Behaviours by Quasi-finality -- Verifying Compiled File System Code -- Reasoning about General Quantum Programs over Mixed States -- A Simple and General Theoretical Account for Abstract Types. |
| Record Nr. | UNINA-9910483264203321 |
| New York ; ; Berlin, : Springer, c2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal Methods and Hybrid Real-Time Systems [[electronic resource] ] : Essays in Honour of Dines Bjorner and Zhou Chaochen on the Occasion of Their 70th Birthdays / / edited by Cliff B. Jones, Zhiming Liu, Jim Woodcock
| Formal Methods and Hybrid Real-Time Systems [[electronic resource] ] : Essays in Honour of Dines Bjorner and Zhou Chaochen on the Occasion of Their 70th Birthdays / / edited by Cliff B. Jones, Zhiming Liu, Jim Woodcock |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (XVI, 542 p.) |
| Disciplina | 004.33 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Computer science Computer engineering Computer networks Machine theory Software Engineering Computer Science Logic and Foundations of Programming Computer Engineering and Networks Formal Languages and Automata Theory |
| ISBN | 3-540-75221-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Models and Software Model Checking of a Distributed File Replication System -- From “Formal Methods” to System Modeling -- A Denotational Semantics for Handel-C -- Generating Polynomial Invariants with DISCOVERER and QEPCAD -- Harnessing rCOS for Tool Support —The CoCoME Experience -- Automating Verification of Cooperation, Control, and Design in Traffic Applications -- Specifying Various Time Models with Temporal Propositional Variables in Duration Calculus -- Relating Domain Concepts Intensionally by Ordering Connections -- Programmable Messaging for Electronic Government - Building a Foundation -- Balancing Insight and Effort: The Industrial Uptake of Formal Methods -- Proving Theorems About JML Classes -- Specification for Testing -- Semantics and Verification of a Language for Modelling Hardware Architectures -- A Domain-Oriented, Model-Based Approach for Construction and Verification of Railway Control Systems -- Compensable Programs -- Deriving Specifications for Systems That Are Connected to the Physical World -- Engineering the Development of Embedded Systems -- Design Verification Patterns -- On Revival of Algol-Concepts in Modern Programming and Specification Languages -- Design in CommUnity with Extension Morphisms -- Symbolic Test Generation Using a Temporal Logic with Constrained Events -- Expansive-Bisimulation for Context-Free Processes -- VDM Semantics of Programming Languages: Combinators and Monads -- Formal Approach to Railway Applications -- Services as a Paradigm of Computation. |
| Record Nr. | UNISA-996465958703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
