Foundations of Computer Software
Modeling, Development, and Verification of Adaptive Systems 16th Monterey Workshop 2010, Redmond, USA, WA, USA, March 31--April 2, Revised Selected Papers
Published on 27. May 2011
250 pages
978-3-642-21292-5 (ISBN)
Description
This book presents the thoroughly refereed and revised post-workshop proceedings of the 16th Monterey Workshop, held in Redmond, WA, USA, in March/April 2010. The theme of the workshop was Foundations of Computer Software, with a special focus on Modeling, Development, and Verification of Adaptive Systems.
The 13 revised full papers presented were carefully reviewed and selected from numerous submissions for inclusion in the book. The contributions show how the foundations and development techniques of computer software could be adapted even for industrial safety-critical and business-critical applications to improve dependability and robustness and to ensure information privacy and security.
More details
Other editions
Additional editions
Radu Calinescu | Ethan Jackson
Foundations of Computer Software
Modeling, Development, and Verification of Adaptive Systems 16th Monterey Workshop 2010, Redmond, USA, WA, USA, March 31--April 2, Revised Selected Papers
Book
05/2011
1st Edition
Springer
€53.49
Shipment within 5-7 days
Content
- Title
- Table of Contents
- Software Verification of Autonomic Systems Developed with ASSL
- Introduction
- ASSL
- Consistency Checking with ASSL
- Built-in Model-Checking Mechanism for ASSL
- Building the Autonomic System Graph
- Building the Model-Checking Engine
- Checking Liveness Properties
- Automatic Test Case Generation with ASSL
- Test Generation Methodology
- Conclusion and Future Work
- References
- Modeling Language Variability
- Introduction
- Language Constituents
- Language Variants
- Classification of Language Variability
- Documentation of Language Variability
- Comparison of Semantic Variants
- Tool Support
- Related Work
- Conclusion
- References
- An Approach for Effective Design Space Exploration
- Introduction
- Motivating Example
- Background on FORMULA
- Representation
- Solving for Instances
- Design Space Exploration Method
- Projection-Based Equivalence Partitioning
- Exploration Algorithms
- Evaluation
- Experimental Setup
- Randomization
- Highly Constrained Design Spaces
- Related Work
- DSE Frameworks
- Exploration Techniques
- DSL Specification Languages
- Discussion and Conclusion
- References
- Migration of Legacy Software Towards Correct-by-Construction Timing Behavior
- Introduction
- Background
- The Timing Definition Language (TDL)
- Aspects of Legacy Controller Systems
- Modeling Timing Behavior of Legacy Controllers with TDL
- Mapping the Legacy Architecture to TDL Constructs
- Implementation of the TDL Operational Semantics
- Activation of Synchronous TDL Tasks
- Data Transfer Operations
- Industrial Application
- Determining the Logical Execution Time
- Testing Results
- Conclusions
- References
- Towards IT Systems Capable of Managing Their Health
- Introduction
- Health Management
- Health Indicators
- Monitoring
- Diagnosis
- Prognosis
- Planning
- Remaining Useful Life Management
- Remediation
- Modeling Framework
- Requirements of a Suitable Model
- Petri Net Basics
- Petri Net Extensions of Interest
- Hierarchy Modeling
- Health Management Modeling Methodology
- Step I - Modeling System Structure and Dependencies
- Step II - Modeling Useful Life Management
- Step III - Modeling Health Recovery
- Step IV - Health Management Policies
- Related Work
- Future Work and Conclusions
- References
- Self-reconfigurable Modular Robots and Their Symbolic Configuration Space
- Introduction
- Problem Statement and Related Works
- Presentation of the CKBot
- Explicit Encoding of CKBot Configurations (from Parkthesis09)
- Compact Representation of Large State Spaces
- Representing CKBot States
- Matrix Representation
- Matrix Encoding
- Symbolic Representation of the CKBot Configuration Space
- Identification of Structural Symmetries
- Symbolic Encoding and Canonization
- Reconfiguration
- Transition Relation Between Symbolic Configurations
- Generating and Exploiting the Symbolic Configuration Space
- Performance Evaluation
- Experiment 1: Generating the Symbolic Configuration Space
- Experiment 2: Computing Paths in the Symbolic Configuration Space
- Conclusion
- References
- Formal Methods @ Runtime
- Introduction
- Quantitative Verification @ Runtime
- Description
- Practical Realisation
- Challenges
- Lightweight Formal Methods @ Runtime
- Description
- Practical Realisation
- Challenges
- Model Checking @ Runtime
- Description
- Practical Realisation
- Challenges
- Other FM@R-Related Approaches
- Conclusion
- References
- Modular State Spaces for Prioritised Petri Nets
- Introduction
- Basic Definitions
- Petri Nets
- Prioritised Petri Nets
- State Spaces of (Prioritised) Petri Nets
- Modular Petri Nets
- Prioritised Modular Petri Nets
- Modular State Spaces
- Algorithms
- Results
- Conclusions
- References
- A Problem Frame-Based Approach to Evolvability: The Case of the Multi-translation
- Introduction
- Proposal of a Specific Problem Frame
- MTF: A Problem Frame for Multi-translation
- Toy-HMS: A Toy-Case Instantiation of MTF
- Relating the Variety of Changes to MTF
- Developing for Change
- Key Principles in Developing for Change
- Guidelines for a MTF-Based Development
- Coping with Changes in the Multi-Translation Frame
- Related Work and Conclusions
- References
- Towards a Framework for Modelling and Verification of Relay Interlocking Systems
- Introduction
- The Railway Application Domain
- Equipment at a Station
- Train Routes and Train Route Tables
- Relay Circuits
- Relay Circuit Diagrams
- Framework Overview
- Domain-Specific Language
- Data Validation
- Simulation
- Verification
- Behavioural Models
- Conditions
- Development of a Domain-Specific Language and Tools
- Conclusions
- References
- Trust Of, In, and among Adaptive Systems
- Introduction
- Adaptation in Mission Critical Systems
- Unlike Redundancy
- An Autonomous Vehicle Problem
- A Mixed Approach May Improve Trust
- Graduated Certification
- Problem of Trust in an Adaptive SOA
- Employing Policy Languages
- Preparing Adaptive Systems for the Real World
- Three Alternative Results
- A Boot Camp
- Summary
- References
- Software Certification: Is There a Case against Safety Cases?
- Introduction
- Software Certification Approaches
- Process Based Approaches
- Product Focused Approaches
- What Do Civil Engineers Do?
- What Can We Learn from Civil Engineering?
- Safety Cases
- Why Safety Cases?
- Some Weaknesses of Safety Cases
- Standards Combining Process and Product Focus with Implicit Safety Cases
- Safety Case Improvements
- Conclusion
- References
- Testing Adaptive Probabilistic Software Components in Cyber Systems
- Introduction
- How Testing for Adaptive Systems Differs from Traditional Testing
- The Scientific Problem
- How to Test Adaptive Systems
- Challenges in Validating Statistical Models for a Wide Range of Operating Environments
- Conclusion
- References
- Author Index
