Jeannette M. Wing, Jim Woodcock, Jim Davies
Proceedings of the World Congress on Formal Methods in the Development of Computing Systems. Volume II
World Congress on Formal Methods, 1999.
@proceedings{FM-v2-1999, address = "Toulouse, France", editor = "Jeannette M. Wing and Jim Woodcock and Jim Davies", isbn = "3-540-66588-9", publisher = "{Springer-Verlag}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the World Congress on Formal Methods in the Development of Computing Systems. Volume II}", volume = 1709, year = 1999, }
Contents (62 items)
- FM-v2-1999-PoizatCR #approach #automaton #concurrent #requirements
- From Informal Requirements to COOP: A Concurrent Automata Approach (PP, CC, JCR), pp. 939–962.
- FM-v2-1999-LangLL #calculus #framework
- A Framework for Defining Object-Calculi (FL, PL, LL), pp. 963–982.
- FM-v2-1999-SeshiaSBD
- A Translation of Statecharts to Esterel (SAS, RKS, AKB, SDD), pp. 983–1007.
- FM-v2-1999-YongG #semantics
- An Operational Semantics for Timed RAISE (XY, CG), pp. 1008–1027.
- FM-v2-1999-Wehrheim #abstraction
- Data Abstraction for CSP-OZ (HW), pp. 1028–1047.
- FM-v2-1999-PolackS #development #using
- Systems Development Using Z Generics (FP, SS), pp. 1048–1067.
- FM-v2-1999-AlexanderRB #summary
- A Brief Summary of VSPEC (PA, MR, PB), pp. 1068–1086.
- FM-v2-1999-LeavensB #specification
- Enhancing the Pre- and Postcondition Technique for More Expressive Specifications (GTL, ALB), pp. 1087–1106.
- FM-v2-1999-Muller-OlmW #on the
- On Excusable and Inexcusable Failures (MMO, AW), pp. 1107–1127.
- FM-v2-1999-VerhoevenB #verification
- Interfacing Program Construction and Verification (RV, RCB), pp. 1128–1146.
- FM-v2-1999-DellacherieDL #linear #programming #verification
- Software Verification Based on Linear Programming (SD, SD, JLL), pp. 1147–1165.
- FM-v2-1999-MahonyD
- Sensors and Actuators in TCOZ (BPM, JSD), pp. 1166–1185.
- FM-v2-1999-Krieg-BrucknerPOB #development #formal method
- The UniForM Workbench, a Universal Development Environment for Formal Methods (BKB, JP, ERO, AB), pp. 1186–1205.
- FM-v2-1999-SchatzH
- Integrating Formal Description Techniques (BS, FH), pp. 1206–1225.
- FM-v2-1999-Merz
- A More Complete TLA (SM), pp. 1226–1244.
- FM-v2-1999-BoerHR #approach #concurrent #paradigm #semantics
- Formal Justification of the Rely-Guarantee Paradigm for Shared-Variable Concurrency: A Semantic Approach (FSdB, UH, WPdR), pp. 1245–1265.
- FM-v2-1999-Martin #first-order #logic
- Relating Z and First-Order Logic (AM), pp. 1266–1280.
- FM-v2-1999-SousaG #component #enterprise #formal method #framework #integration #modelling
- Formal Modeling of the Enterprise JavaBeansTM Component Integration Framework (JPS, DG), pp. 1281–1300.
- FM-v2-1999-MikhajlovSL #component
- Developing Components in the Presence of Re-entrance (LM, ES, LL), pp. 1301–1320.
- FM-v2-1999-Jonkers #communication #interactive #using
- Communication and Synchronisation Using Interaction Objects (HBMJ), pp. 1321–1342.
- FM-v2-1999-Feijs #modelling #using #π-calculus
- Modelling Microsoft COM Using π-Calculus (LMGF), pp. 1343–1363.
- FM-v2-1999-SmarandacheGG #calculus #constraints #realtime #validation
- Validation of Mixed SIGNAL-ALPHA Real-Time Systems through Affine Calculus on Clock Synchronisation Constraints (IMS, TG, PLG), pp. 1364–1383.
- FM-v2-1999-Nadjm-TehraniA #design #modelling #proving #theorem proving
- Combining Theorem Proving and Continuous Models in Synchronous Design (SNT, OÅ), pp. 1384–1399.
- FM-v2-1999-IyodaSS #clustering #named
- ParTS: A Partitioning Transformation System (JI, AS, LS), pp. 1400–1419.
- FM-v2-1999-Jifeng #behaviour #co-evolution #design
- A Behavioral Model for Co-design (JH), pp. 1420–1438.
- FM-v2-1999-CavalcantiN #object-oriented #refinement #semantics
- A Weakest Precondition Semantics for an Object-Oriented Language of Refinement (AC, DAN), pp. 1439–1459.
- FM-v2-1999-BackMW #interactive #reasoning
- Reasoning About Interactive Systems (RJB, AM, JvW), pp. 1460–1476.
- FM-v2-1999-DerrickB #refinement
- Non-atomic Refinement in Z (JD, EAB), pp. 1477–1496.
- FM-v2-1999-HehnerG #refinement #semantics
- Refinement Semantics and Loop Rules (ECRH, AMG), pp. 1497–1510.
- FM-v2-1999-ChaudronTW #design #formal method #lessons learnt
- Lessons from the Application of Formal Methods to the Design of a Storm Surge Barrier Control System (MRVC, JT, KW), pp. 1511–1526.
- FM-v2-1999-KingHCP #experience #industrial #proving #verification
- The Value of Verification: Positive Experience of Industrial Proof (SK, JH, RC, AP), pp. 1527–1545.
- FM-v2-1999-HaxthausenP #development #distributed #verification
- Formal Development and Verification of a Distributed Railway Control System (AEH, JP), pp. 1546–1563.
- FM-v2-1999-SereT #analysis #safety #specification
- Safety Analysis in Formal Specification (KS, ET), pp. 1564–1583.
- FM-v2-1999-CimattiPSTV #communication #protocol #specification #validation
- Formal Specification and Validation of a Vital Communication Protocol (AC, PLP, RS, PT, AV), pp. 1584–1604.
- FM-v2-1999-MarchandS #design #incremental #synthesis #using
- Incremental Design of a Power Transformer Station Controller Using a Controller Synthesis Methodology (HM, MS), pp. 1605–1624.
- FM-v2-1999-MoriF #behaviour #specification #verification
- Verifying Behavioural Specifications in CafeOBJ Environment (AM, KF), pp. 1625–1643.
- FM-v2-1999-DiaconescuFI #algebra #component #specification #verification
- Component-Based Algebraic Specification and Verification in CafeOBJ (RD, KF, SI), pp. 1644–1663.
- FM-v2-1999-Nakajima #algebra #development #framework #object-oriented #specification #using
- Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks (SN), pp. 1664–1683.
- FM-v2-1999-ClavelDEMS #maude
- Maude as a Formal Meta-tool (MC, FD, SE, JM, MOS), pp. 1684–1703.
- FM-v2-1999-GoguenR #algebra
- Hiding More of Hidden Algebra (JAG, GR), pp. 1704–1719.
- FM-v2-1999-Eschbach #algorithm #detection #specification #termination #verification
- A Termination Detection Algorithm: Specification and Verification (RE), pp. 1720–1737.
- FM-v2-1999-GradelS #state machine
- Logspace Reducibility via Abstract State Machines (EG, MS), pp. 1738–1757.
- FM-v2-1999-DunstanKML #formal method
- Formal Methods for Extensions to CAS (MD, TK, UM, SL), pp. 1758–1777.
- FM-v2-1999-JimenezO #algebra #framework #higher-order
- An Algebraic Framework for Higher-Order Modules (RMJ, FO), pp. 1778–1797.
- FM-v2-1999-RandimbivololonaSBPRS #approach #proving
- Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach (FR, JS, PB, AP, JR, DS), pp. 1798–1815.
- FM-v2-1999-GarbettPSA #empirical #process #synthesis
- Secure Synthesis of Code: A Process Improvement Experiment (PG, JPP, MS, SA), pp. 1816–1835.
- FM-v2-1999-HainquePBN #compilation #composition #named #tool support
- Cronos: A Separate Compilation Toolset for Modular Esterel Applications (OH, LP, YLB, EN), pp. 1836–1853.
- FM-v2-1999-KnightFH #tool support #using
- Tool Support for Production Use of Formal Techniques (JCK, PTF, BRH), p. 1854.
- FM-v2-1999-DongMF #modelling
- Modeling Aircraft Mission Computer Task Rates (JSD, BPM, NF), p. 1855.
- FM-v2-1999-HabriasPL #case study #collaboration #specification
- A Study of Collaborative Work: Answers to a Test on Formal Specification in B (HH, PP, JYL), pp. 1856–1857.
- FM-v2-1999-KellomakiM #design #logic
- Archived Design Steps in Temporal Logic (PK, TM), p. 1858.
- FM-v2-1999-LevyT #approach #education
- A PVS-Based Approach for Teaching Constructing Correct Iterations (ML, LT), pp. 1859–1860.
- FM-v2-1999-Baumgarten #framework #specification
- A Minimal Framework for Specification Theory (BB), p. 1861.
- FM-v2-1999-MacCollC #interactive #testing
- A Model of Specification-Based Testing of Interactive Systems (IM, DAC), p. 1862.
- FM-v2-1999-OcicaI #algebra #aspect-oriented #corba #syntax
- Algebraic Aspects of the Mapping between Abstract Syntax Notation One and CORBA IDL (RO, DI), p. 1863.
- FM-v2-1999-BanachP
- Retrenchment (RB, MP), pp. 1864–1865.
- FM-v2-1999-Moreira #component #proving
- Proof Preservation in Component Generalization (AMM), p. 1866.
- FM-v2-1999-HorsteS #formal method #modelling #petri net #simulation #using
- Formal Modelling and Simulation of Train Control Systems Using Petri Nets (MMzH, ES), p. 1867.
- FM-v2-1999-HorlA #communication #specification
- Formal Specification of a Voice Communication System Used in Air Traffic Control (JH, BKA), p. 1868.
- FM-v2-1999-ButhS #architecture #communication #design #model checking
- Model-Checking the Architectural Design of a Fail-Safe Communication System for Railway Interlocking Systems (BB, MS), p. 1869.
- FM-v2-1999-Droschl #data access #requirements #using
- Analyzing the Requirements of an Access Control Using VDMTools and PVS (GD), p. 1870.
- FM-v2-1999-AkhianiDHLSTY #verification
- Cache Coherence Verification with TLA+ (HA, DD, PH, LL, JS, MRT, YY), pp. 1871–1872.
10 ×#specification
8 ×#verification
7 ×#using
6 ×#design
5 ×#algebra
5 ×#formal method
5 ×#framework
5 ×#modelling
4 ×#approach
4 ×#communication
8 ×#verification
7 ×#using
6 ×#design
5 ×#algebra
5 ×#formal method
5 ×#framework
5 ×#modelling
4 ×#approach
4 ×#communication