This book constitutes the refereed proceedings of the 6th International Conference on Algebraic Methodology and Software Engineering, AMAST'97, held in Sydney, Australia, in December 1997. The volume presents 48 revised full papers selected from an unusually high number of submissions. One of the outstanding features of AMAST is its mix of serious mathematical development of formal methods in software engineering with practical concerns, tools, case studies, and industrial development. The volume addresses all current aspects of formal methods in software engineering and programming methodology, with a certain emphasis on algebraic and logical foundations.
Author(s): Slim Ben Lamine, John Plaice (auth.), Michael Johnson (eds.)
Series: Lecture Notes in Computer Science 1349
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1997
Language: English
Pages: 602
Tags: Software Engineering; Logics and Meanings of Programs; Special Purpose and Application-Based Systems; Mathematical Logic and Formal Languages; Programming Techniques
Software configuration with information systems....Pages 1-15
Head-tactics simplification....Pages 16-29
Iteration 2-theories: Extended Abstract ....Pages 30-44
Model checking and fault tolerance....Pages 45-59
Deadlock analysis for a fault-tolerant system....Pages 60-74
From sequential to multi-threaded Java: An event-based operational semantics....Pages 75-90
Permissive subsorted partial logic in CASL....Pages 91-107
Specification of timing constraints within the circal process algebra....Pages 108-122
On the specification and verification of performance properties for a timed process algebra....Pages 123-137
Abstract interpretation of algebraic polynomial systems (Extended abstract)....Pages 138-154
Modular refinement and model building....Pages 155-169
A linear temporal logic approach to objects with transactions....Pages 170-184
Software design, specification, and verification: Lessons learned from the Rether case study....Pages 185-198
Refinement rules for real-time multi-tasking programs....Pages 199-215
Rigorous object-oriented modeling: Integrating formal and informal notations....Pages 216-230
Completeness in abstract interpretation: A domain perspective....Pages 231-245
Floating point verification in HOL light: The exponential function....Pages 246-260
Verification of distributed real-time and fault-tolerant protocols....Pages 261-275
Invariants, bisimulations and the correctness of coalgebraic refinements....Pages 276-291
On bisimulation, fault-monotonicity and provable fault-tolerance....Pages 292-306
Span(Graph): A categorical algebra of transition systems....Pages 307-321
Representing place/transition nets in Span(Graph)....Pages 322-336
Invariants of parameterized binary tree networks as greatest fixpoints....Pages 337-350
Modelling specification construction by successive approximations....Pages 351-364
On partial validation of logic programs....Pages 365-379
Preservation and reflection in specification....Pages 380-394
Case studies in using a meta-method for formal method integration....Pages 395-408
The update calculus....Pages 409-423
Selective attribute elimination for categorical data specifications....Pages 424-436
ATM switch design: Parametric high-level modeling and formal verification....Pages 437-450
The hidden function question revisited....Pages 451-464
Synchronization of logics with mixed rules: Completeness preservation....Pages 465-478
Symbolic bisimulation for Full LOTOS....Pages 479-493
Algebraic composition and refinement of proofs....Pages 494-508
Ensuring streams flow....Pages 509-523
Extending process languages with time....Pages 524-538
Parametric analysis of computer systems....Pages 539-553
CAMILA: Prototyping and refinement of constructive specifications....Pages 554-559
PAMELA+PVS....Pages 560-562
The circal system....Pages 563-564
A refinement-type checker for standard ML....Pages 565-566
Recording HOL proofs in a structured browsable format....Pages 567-571
Analysing multi-agent system traces with ID a F....Pages 572-573
DOVE: A tool for design oriented verification and evaluation....Pages 574-575
The B method and the B toolkit....Pages 576-580
An algebraic language processing environment....Pages 581-585
The Cogito development system....Pages 586-591
