FM 2008: Formal Methods [[electronic resource] ] : 15th International Symposium on Formal Methods, Turku, Finland, May 26-30, 2008, Proceedings / / edited by Jorge Cuellar, Tom Maibaum |
Edizione | [1st ed. 2008.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 |
Descrizione fisica | 1 online resource (XIII, 436 p.) |
Disciplina | 005.1 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Computer engineering Computer programming Computer logic Programming languages (Electronic computers) Software Engineering/Programming and Operating Systems Computer Engineering Programming Techniques Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters |
ISBN | 3-540-68237-6 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Session 1. Invited Talks -- Aspects and Formal Methods -- Getting Formal Verification into Design Flow -- Lessons in the Weird and Unexpected: Some Experiences from Checking Large Real Systems -- Simulation, Orchestration and Logical Clocks -- Session 2. Programming Language Analysis -- CoVaC: Compiler Validation by Program Analysis of the Cross-Product -- Lazy Behavioral Subtyping -- Checking Well-Formedness of Pure-Method Specifications -- Session 3. Verification -- Verifying Dynamic Pointer-Manipulating Threads -- Proofs and Refutations for Probabilistic Refinement -- Assume-Guarantee Verification for Interface Automata -- Session 4. Real-Time and Concurrency -- Automated Verification of Dense-Time MTL Specifications Via Discrete-Time Approximation -- A Model Checking Language for Concurrent Value-Passing Systems -- Session 5. Grand Chellenge Problems -- Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code -- Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM -- Session 6. FM Practice -- Industrial Use of Formal Methods for a High-Level Security Evaluation -- Secret Ninja Formal Methods -- Specification and Checking of Software Contracts for Conditional Information Flow -- Session 7. Runtime Moitoring and Analysis -- JML Runtime Assertion Checking: Improved Error Reporting and Efficiency Using Strong Validity -- Provably Correct Runtime Monitoring -- Session 8. Communication -- A Schedulerless Semantics of TLM Models Written in SystemC Via Translation into LOTOS -- A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service -- Session 9. Constraint Analysis -- Constraint Prioritization for Efficient Analysis of Declarative Models -- Finding Minimal Unsatisfiable Cores of Declarative Specifications -- Precise Interval Analysis vs. Parity Games -- Session 10. Design -- Introducing Objects through Refinement -- Masking Faults While Providing Bounded-Time Phased Recovery -- Towards Consistent Specifications of Product Families -- Session 11. Industry Day -- Formal Methods for Trustworthy Skies: Building Confidence in the Security of Aircraft Assets Distribution -- An Industrial Case: Pitfalls and Benefits of Applying Formal Methods to the Development of a Network-Centric RTOS -- Software Engineering with Formal Methods: Experiences with the Development of a Storm Surge Barrier Control System -- Application of a Formal Specification Language in the Development of the “Mobile FeliCa” IC Chip Firmware for Embedding in Mobile Phone -- Safe and Reliable Metro Platform Screen Doors Control/Command Systems. |
Record Nr. | UNISA-996465640803316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Methods at the Crossroads. From Panacea to Foundational Support [[electronic resource] ] : 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18-20, 2002, Revised Papers / / edited by Bernhard K. Aichernig, Tom Maibaum |
Edizione | [1st ed. 2003.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 |
Descrizione fisica | 1 online resource (XIV, 462 p.) |
Disciplina | 005.1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Computer science Programming languages (Electronic computers) Computer logic Mathematical logic Software Engineering/Programming and Operating Systems Software Engineering Computer Science, general Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages |
ISBN | 3-540-40007-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | In Memoriam Armando Martín Haeberer -- In Memoriam Armando Martín Haeberer -- Work at UNU/IIST -- UNU and UNU/IIST -- Contract-Based Testing -- The Development of the RAISE Tools -- An Algebraic Approach to the VERILOG Programming -- Real-Time Systems Development with Duration Calculi: An Overview -- X2Rel: An XML Relation Language with Formal Semantics -- At the Crossroads -- Where, Exactly, Is Software Development? -- From Formal Techniques to Well-Founded Software Development Methods -- Towards the Verifying Compiler -- A Grand Challenge Proposal for Formal Methods: A Verified Stack -- “What Is an Infrastructure?” Towards an Informatics Answer -- A Formal Basis for Some Dependability Notions -- From Models to Software -- Multi-view Modeling of Software Systems -- An Executable Specification Language Based on Message Sequence Charts -- Graph-Based Models of Internetworking Systems -- Software Development by Refinement -- Formal Methods within a Totally Functional Approach to Programming -- Coordination Technologies for Just-in-Time Integration -- Real-Time Systems -- Real-Time Process Algebra and Its Applications -- Making Timed Automata Communicate -- A Tool Architecture for the Next Generation of Uppaal -- Verification -- Verification by Abstraction -- Combining Decision Procedures -- A Theory of Hints in Model Checking -- Type Systems for Concurrent Programs. |
Record Nr. | UNISA-996465962703316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Methods at the Crossroads. From Panacea to Foundational Support : 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18-20, 2002, Revised Papers / / edited by Bernhard K. Aichernig, Tom Maibaum |
Edizione | [1st ed. 2003.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 |
Descrizione fisica | 1 online resource (XIV, 462 p.) |
Disciplina | 005.1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Computer science Programming languages (Electronic computers) Computer logic Mathematical logic Software Engineering/Programming and Operating Systems Software Engineering Computer Science, general Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages |
ISBN | 3-540-40007-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | In Memoriam Armando Martín Haeberer -- In Memoriam Armando Martín Haeberer -- Work at UNU/IIST -- UNU and UNU/IIST -- Contract-Based Testing -- The Development of the RAISE Tools -- An Algebraic Approach to the VERILOG Programming -- Real-Time Systems Development with Duration Calculi: An Overview -- X2Rel: An XML Relation Language with Formal Semantics -- At the Crossroads -- Where, Exactly, Is Software Development? -- From Formal Techniques to Well-Founded Software Development Methods -- Towards the Verifying Compiler -- A Grand Challenge Proposal for Formal Methods: A Verified Stack -- “What Is an Infrastructure?” Towards an Informatics Answer -- A Formal Basis for Some Dependability Notions -- From Models to Software -- Multi-view Modeling of Software Systems -- An Executable Specification Language Based on Message Sequence Charts -- Graph-Based Models of Internetworking Systems -- Software Development by Refinement -- Formal Methods within a Totally Functional Approach to Programming -- Coordination Technologies for Just-in-Time Integration -- Real-Time Systems -- Real-Time Process Algebra and Its Applications -- Making Timed Automata Communicate -- A Tool Architecture for the Next Generation of Uppaal -- Verification -- Verification by Abstraction -- Combining Decision Procedures -- A Theory of Hints in Model Checking -- Type Systems for Concurrent Programs. |
Record Nr. | UNINA-9910144027803321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Fundamental Approaches to Software Engineering [[electronic resource] ] : Third International Conference, FASE 2000 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2000 Berlin, Germany, March 25 - April 2, 2000 Proceedings / / edited by Tom Maibaum |
Edizione | [1st ed. 2000.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 |
Descrizione fisica | 1 online resource (XIII, 378 p.) |
Disciplina | 005.1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer logic Software Engineering/Programming and Operating Systems Software Engineering Programming Languages, Compilers, Interpreters Logics and Meanings of Programs |
ISBN | 3-540-46428-X |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Papers -- Essay on Software Engineering at the Turn of Century -- Memex Is Not Enough -- From Play-In Scenarios to Code: An Achievable Dream -- Real-Time Systems -- Parallel Refinement Mechanisms for Real-Time Systems -- Applying RT-Z to Develop Safety-Critical Systems -- A Process Algebra for Real-Time Programs -- Formally Engineering Systems -- System Fault Tolerance Specification: Proposal of a Method Combining Semi-formal and Formal Approaches -- Structuring and Design of Reactive Systems Using RSDS and B -- Using Domain-Specific Languages for the Realization of Component Composition -- Software Engineering -- Analysing UML Active Classes and Associated State Machines - A Lightweight Formal Approach -- Software as Learning: Quality Factors and Life-Cycle Revised -- What Is ‘Mathematicalness’ in Software Engineering? -- A Formal Approach to Heterogeneous Software Modeling -- Object Orientation -- Formal Specification of Object-Oriented Meta-modelling -- Verification of Object Oriented Programs Using Class Invariants -- Verification of Object-Z Specifications by Using Transition Systems: Application to the Radiomobile Network Design Problem -- A Model for Describing Object-Oriented Systems from Multiple Perspectives -- Formally Engineering Systems -- Stepwise Introduction and Preservation of Safety Properties in Algebraic High-Level Net Systems -- Theory and Applications -- Ready-Simulation Is Not Ready to Express a Modular Refinement Relation -- Java Program Verification via a Hoare Logic with Abrupt Termination -- Foundations for Software Configuration Management Policies Using Graph Transformations -- Analyzing Non-functional Properties of Mobile Agents -- Case Studies -- Specification of an Automatic Manufacturing System: A Case Study in Using Integrated Formal Methods -- A Case Study on Using Automata in Control Synthesis -- Demonstrations -- Formal System Development with KIV -- More About TAS and IsaWin — Tools for Formal Program Development -- Using Maude. |
Record Nr. | UNISA-996465609403316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Fundamental Approaches to Software Engineering : Third International Conference, FASE 2000 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2000 Berlin, Germany, March 25 - April 2, 2000 Proceedings / / edited by Tom Maibaum |
Edizione | [1st ed. 2000.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 |
Descrizione fisica | 1 online resource (XIII, 378 p.) |
Disciplina | 005.1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer logic Software Engineering/Programming and Operating Systems Software Engineering Programming Languages, Compilers, Interpreters Logics and Meanings of Programs |
ISBN | 3-540-46428-X |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Papers -- Essay on Software Engineering at the Turn of Century -- Memex Is Not Enough -- From Play-In Scenarios to Code: An Achievable Dream -- Real-Time Systems -- Parallel Refinement Mechanisms for Real-Time Systems -- Applying RT-Z to Develop Safety-Critical Systems -- A Process Algebra for Real-Time Programs -- Formally Engineering Systems -- System Fault Tolerance Specification: Proposal of a Method Combining Semi-formal and Formal Approaches -- Structuring and Design of Reactive Systems Using RSDS and B -- Using Domain-Specific Languages for the Realization of Component Composition -- Software Engineering -- Analysing UML Active Classes and Associated State Machines - A Lightweight Formal Approach -- Software as Learning: Quality Factors and Life-Cycle Revised -- What Is ‘Mathematicalness’ in Software Engineering? -- A Formal Approach to Heterogeneous Software Modeling -- Object Orientation -- Formal Specification of Object-Oriented Meta-modelling -- Verification of Object Oriented Programs Using Class Invariants -- Verification of Object-Z Specifications by Using Transition Systems: Application to the Radiomobile Network Design Problem -- A Model for Describing Object-Oriented Systems from Multiple Perspectives -- Formally Engineering Systems -- Stepwise Introduction and Preservation of Safety Properties in Algebraic High-Level Net Systems -- Theory and Applications -- Ready-Simulation Is Not Ready to Express a Modular Refinement Relation -- Java Program Verification via a Hoare Logic with Abrupt Termination -- Foundations for Software Configuration Management Policies Using Graph Transformations -- Analyzing Non-functional Properties of Mobile Agents -- Case Studies -- Specification of an Automatic Manufacturing System: A Case Study in Using Integrated Formal Methods -- A Case Study on Using Automata in Control Synthesis -- Demonstrations -- Formal System Development with KIV -- More About TAS and IsaWin — Tools for Formal Program Development -- Using Maude. |
Record Nr. | UNINA-9910143635703321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
On the Construction of Engineering Handbooks [[electronic resource] ] : with an Illustration from the Railway Safety Domain / / by Stefan Gruner, Apurva Kumar, Tom Maibaum, Markus Roggenbach |
Autore | Gruner Stefan |
Edizione | [1st ed. 2020.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 |
Descrizione fisica | 1 online resource (XII, 83 p. 13 illus., 6 illus. in color.) |
Disciplina | 808.0666 |
Collana | SpringerBriefs in Computer Science |
Soggetto topico |
Software engineering
Management information systems Computer science Computers Law and legislation Transportation engineering Traffic engineering Software Engineering Management of Computing and Information Systems Legal Aspects of Computing Transportation Technology and Traffic Engineering |
ISBN | 3-030-44648-4 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | I Part I : Background -- 1Introduction and Motivation -- 2Related Work -- Part II : Analysis -- 3A General Method for Composing an Engineering HB -- 4Application of the General Method to the Railway Domain -- Part III : Synthesis -- 5Example HB Entry of a Formal Method for the Railway Domain - Step 6 -- 6Conclusions and Prospects for Future Work. . |
Record Nr. | UNISA-996465448303316 |
Gruner Stefan | ||
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
On the Construction of Engineering Handbooks : with an Illustration from the Railway Safety Domain / / by Stefan Gruner, Apurva Kumar, Tom Maibaum, Markus Roggenbach |
Autore | Gruner Stefan |
Edizione | [1st ed. 2020.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 |
Descrizione fisica | 1 online resource (XII, 83 p. 13 illus., 6 illus. in color.) |
Disciplina | 808.0666 |
Collana | SpringerBriefs in Computer Science |
Soggetto topico |
Software engineering
Management information systems Computer science Computers Law and legislation Transportation engineering Traffic engineering Software Engineering Management of Computing and Information Systems Legal Aspects of Computing Transportation Technology and Traffic Engineering |
ISBN | 3-030-44648-4 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | I Part I : Background -- 1Introduction and Motivation -- 2Related Work -- Part II : Analysis -- 3A General Method for Composing an Engineering HB -- 4Application of the General Method to the Railway Domain -- Part III : Synthesis -- 5Example HB Entry of a Formal Method for the Railway Domain - Step 6 -- 6Conclusions and Prospects for Future Work. . |
Record Nr. | UNINA-9910409675903321 |
Gruner Stefan | ||
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|