Ebook: Algebraic Methodology and Software Technology: 9th International Conference, AMAST 2002 Saint-Gilles-les-Bains, Reunion Island, France September 9–13, 2002 Proceedings

This volume contains the proceedings of AMAST 2002, the 9th International Conference on Algebraic Methodology and Software Technology, held during September 9–13, 2002, in Saint-Gilles-les-Bains, R´eunion Island, France. The major goal of the AMAST conferences is to promote research that may lead to setting software technology on a ?rm mathematical basis. This goal is achieved through a large international cooperation with contributions from both academia and industry. Developing a software technology on a mathematical basis p- duces software that is: (a) correct, and the correctness can be proved mathem- ically, (b) safe, so that it can be used in the implementation of critical systems, (c) portable, i. e. , independent of computing platforms and language generations, (d) evolutionary, i. e. , it is self-adaptable and evolves with the problem domain. All previous AMAST conferences, which were held in Iowa City (1989, 1991), Twente (1993), Montreal (1995), Munich (1996), Sydney (1997), Manaus (1999), and Iowa City (2000), made contributions to the AMAST goals by reporting and disseminating academic and industrial achievements within the AMAST area of interest. During these meetings, AMAST attracted an international following among researchers and practitioners interested in software technology, progr- ming methodology, and their algebraic, and logical foundations.

---

This book constitutes the refereed proceedings of the 9th International Conference on Algebraic Methodology and Software Technology, AMAST 2002, held in Saint-Gilles-les-Bains, Reunion Island, France in September 2002. The 26 revised full papers presented together with 6 invited papers and 2 system descriptions were carefully reviewed and selected from 59 submissions. Among the topics covered are all current issues in formal methods related to algebraic approaches including abstract data types, process algebras, algebraic specification, semantic specification, model checking, mu-calculus, Petri box algebras, unification, verification of Java for smart cards, security, JML specification, and formal software development. Table of Contents Cover Algebraic Methodology and SoftwareTechnology - 9th International Conference, AMAST 2002 Saint-Gilles-les-Bains, Reunion Island, France September 9-13, 2002, Proceedings ISBN 3540441441 Preface Program Committee Chairs External Reviewers Table of Contents From Specifications to Code in CASL A Taste of Casl Specifications and Programs Some Unresolved Issues Models of Programs vs. Models of Specifications Relationships between Levels and between Languages Conclusion References Automata and Games for Synthesis Generalization of the Setting Comparing Controllers Decentralized Control Related Work Pragmatics of Modular SOS Introduction Foundations Illustrative Examples Simple Expressions Bindings Stores Exceptions Interaction Pragmatic Aspects Tool Support Why not Big Steps? Conclusion Acknowledgements Tool-Assisted Specification and Verification of the JavaCard Platform An Overview of CertiCartes Module BCV Constructing Certified Abstractions with Jakarta The Jakarta Transformation Kit Synthesis of the Offensive JCVM Synthesis of the Abstract JCVM Automating Cross-Validation of Virtual Machines Summary Higher-Order Quantification and Proof Search Introduction Entailment Generally Needs Induction Quantification at Function and Predicate Types Reversing a List Is Symmetric Two Implementations of a Counter Multiset Rewriting in Proof Search Security Protocols in Proof Search Encryption as an Abstract Datatype Abstracting over Internal States of Agents Conclusion Algebraic Support for Service-Oriented Architecture Why Object-Oriented Techniques Cannot Address Them Orchestration through Coordination Algebraic Support A Simple Example References Fully Automatic Adaptation of Software Components Based on Semantic Specifications Introduction The Problem of Unstable Interfaces The AxML Language for Synthesis Requests o Synthesis Requests. o A Further Benefit: Recognition of Semantic Errors. An Overview of AxML Specification Axioms. Synthesis Requests. Synthesis Methods Search o Phase 2: Unification up to -Equality. o Phase 4: Soundness Check for Observational Equality. Related Work Automatic Retrieval, Adaptation and Composition. Conclusion and Future Directions Automatic Composition of Generic Library Functions. HasCasl: Towards Integrated Specification and Development of Functional Programs The Basic HasCasl Logic Signatures and Sentences Models and Satisfaction Type Classes and Polymorphism Predicates and Non-strict Functions Internal Equality and the Internal Logic Recursive Functions From HasCasl Specifications to Haskell Programs - An Example Conclusions and Future Work Acknowledgements Removing Redundant Arguments of Functions Preliminaries Redundant Arguments Redundancy of Positions Using Redundant Positions for Characterizing Redundancy Erasing Redundant Arguments Conclusion Related Work References A Class of Decidable Parametric Hybrid Systems The Model Syntax Semantics o Continuous Evolutions. Forward Analysis Weakly-Controlled Hybrid Automata Remarks Weakly-Controlled and Forward Analysis o Proof. Computing the Reachable States of a Weakly-Controlled Hybrid Automaton Proof of the Theorem o Preliminaries. o Crossing a Minimal Weakly-Controlled Word. o End of the Proof. Finding Bisimulation Statements o Bisimilarity. Cylindrical Algebraic Decomposition o Definition. State Equivalence ~ o Discrete Successor of a Block which Are Not in the Tree. References Vacuity Checking in the Modal Mu-Calculus Vacuity in the Modal Mu-Calculus The Modal Mu-Calculus is a Logic with Polarity Algorithm for Redundancy Detection Case Studies and Performance Measurements Case Study 2: Rether (XMC) Case Study 3: Railway Interlocking System (CWB-NC) Conclusions On Solving Temporal Logic Queries Temporal Logic Queries Syntax of Temporal Logics Temporal Queries Relevant Solutions The Lattice of Solutions Bounding the Number of Minimal Solutions Polynomial-Time Algorithms for Temporal Queries Deciding Minimality Computing Unique Minimal Solutions Counting the Minimal Solutions Conclusions Acknowledgments Modelling Concurrent Behaviours by Commutativity and Weak Causality Relations Relational Structure Model of Concurrency Generalized Order Structures and Concurrent Histories Conclusive Remarks References An Algebra of Non-safe Petri Boxes An Algebra of Boxes An Algebra of Asynchronous Box Expressions Causality in Boxes and Box Expressions Concluding Remarks Refusal Simulation and Interactive Games Introduction Basic Observations and Style of Definition Refusal Simulation Rooted Refusal Simulation Interactive Games and Refusal Simulation Games for Rooted Refusal Simulation Formats for Refusal Simulations SOS Rules with Orderings Conditions on OSOS Rules and Orderings Refusal Simulation Format Conclusion References A Theory of May Testing for Asynchronous Calculi with Locality and No Name Matching The Calculus Lp= The Calculus Lp An Axiomatization of Finitary Lp= and Lp Related Work References Equational Axioms for Probabilistic Bisimilarity Preliminaries Axioms of Iteration Algebras An Equational Axiomatization of Probabilistic Bisimilarity Soundness Normal Forms Completeness References Bisimulation by Unification Notation Formulae as Labels Large Symbolic Bisimulation Bisimulation by Unification Algebraic PC without Structural Axioms Algebraic PC with AC1 Parallel Composition Operator Case Study: A Basic Calculus for Mobility Conclusions Acknowledgements Transforming Processes to Check and Ensure Information Flow Security Basic Notions Defining P_BNDC Processes The t Completion of a Process Checking P_BNDC An Example Conclusions References On Bisimulations for the Spi Calculus Language Environment-Sensitive Bisimulations Alley and Trellis Bisimulations Hedged Bisimulation Bisimilarities Distinguishing Examples Framed vs Hedged Comparing Bisimulations References Specifying and Verifying a Decimal Representation in Java for Smart Cards Introduction Specifying Java Source Code Decimal Class Specification Representing JML-Annotated Java in PVS Decimal Class Verification Verifying void add(short,short) Decimal Multiplication Conclusions A Method for Secure Smartcard Applications The Method in a Nutshell Specification of the Example Security Properties and the Attacker Specification of the Protocols From Diagrams to Algebraic Specifications Correctness of the Card Implementation Related Work References Extending JML Specifications with Temporal Logic The Java Modeling Language Specification Patterns Temporal Specifications in JML An Example: Temporal Aspects of the JCSystem Class Semantics Translating Temporal Formulae Back to JML Conclusions and Future Work Algebraic Dynamic Programming Introduction Overview of Our Approach Dynamic Programming, Traditional Style Related Problems Algebraic Dynamic Programming Representing the Search Space by a Term Algebra Evaluation Algebras Yield Grammars The ADP Programming System An ASCII Notation for Annotated Yield Grammars Programming Methodology Connecting Related Problems: From Global to Local Pattern Matching Controlling Efficiency: Width Reduction o Splitting Words The Taming of the Near-Optimal Solution Space References Analyzing String Buffers in C Introduction Conservative Overrun Analysis The String CLanguage and Its Semantics Instrumented Operational Semantics Abstract Domains Polyhedral Buffer Domain Possible and Definite Buffer Sharing Domains Domain Interaction Abstract Semantics for String C Non-array Statements Array Statements Control Statements Future Work A Foundation of Escape Analysis Preliminaries The Property E Implementation Discussion References A Framework for Order-Sorted Algebra Introduction Variants of Order-Sorted Algebra A Proposed Framework for Order-Sorted Algebra Categories of Order-Sorted Sets Order-Sorted Theories o Monads Three Forms of Order-Sorted Algebra Signatures and Algebras Relating Categories of Order Sorted Sets Description as Lax Slice Categories The Connection with Partial Algebras Example of Theory as Category The Classifying Category of an Order-Sorted Theory Construction of the Classifying Category from a Signature Presentations Including Equations Conclusions and Further Work Guarded Transitions in Evolving Specifications Introduction State Machines and Algebraic Specifications Guards as Arrows Construction Examples Full Construction o Examples Adjoining Guards to Spec Concluding Remarks Revisiting the Categorical Approach to Systems Capturing Constraints on Configurations Horizontal vs Vertical Structuring Compositionality Conclusions Proof Transformations for Evolutionary Formal Software Development Evolutionary Formal Software Development Development Transformations Basic Transformations Extending/Restricting the Signature Changing Existing Signature Entries Adding/Removing Proof Obligations and Assumptions Changing Formulae o Wrap Quantifier. Changing Induction Schemes Completeness and Adequacy Supporting Basic Transformations Conclusions and Future Work References Sharing Objects by Read-Only References Introduction Outline The Mode System A Brief Example Formal Description of the Mode System The Type System Dynamic Semantics Read-Only Properties Discussion Conclusion and Future Work Class-Based versus Object-Based: A Denotational Comparison Syntax Preliminaries Object-Based Denotational Semantics Class-Based Object-Based Logics of Programs Class-Based Object-Based Comparison Conclusion References BRAIN: Backward Reachability Analysis with Integers Why Backward Reachability The Reachability Algorithm Availability References The Development Graph Manager Maya From Textual to Logical Representation Verification In-the-Large Verification In-the-Small Evolution of Developments References Author Index