The Community for Technology Leaders
Industrial-Strength Formal Specification Techniques, Workshop on (1995)
Boca Raton, Florida
Apr. 5, 1995 to Apr. 8, 1995
ISBN: 0-8186-7005-3
TABLE OF CONTENTS

Foreword (PDF)

pp. vii

Committees (PDF)

pp. viii
Session 1

Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods (Abstract)

S.P. Miller , Collins Commercial Avionics, Rockwell Int. Corp., Cedar Rapids, IA, USA
M. Srivas , Collins Commercial Avionics, Rockwell Int. Corp., Cedar Rapids, IA, USA
pp. 2

The architectural specification of an avionic subsystem (Abstract)

L. Spencer , Dept. of Comput., Open Univ., Milton Keynes, UK
J.S. Fitzgerald , Dept. of Comput., Open Univ., Milton Keynes, UK
L.M. Barroca , Dept. of Comput., Open Univ., Milton Keynes, UK
pp. 17

Experiences in applying formal methods to the analysis of software and system requirements (Abstract)

G. Cleland , Lab. for Found. of Comput. Sci., Edinburgh Univ., UK
C. Kirkwood , Dept. of Comput. Sci., Glasgow Univ., UK
M.G. Staskauskas , Dept. of Core Switching Dev., AT&T Bell Labs., Naperville, IL, USA
S.P. Miller , Collins Commercial Avionics, Rockwell Int. Corp., Cedar Rapids, IA, USA
R. Covington , Loral SIS, Houston, TX, USA
A.R. Flora-Holmquist , Dept. of Core Switching Dev., AT&T Bell Labs., Naperville, IL, USA
D. MacKenzie , Lab. for Found. of Comput. Sci., Edinburgh Univ., UK
D. Hamilton , Loral SIS, Houston, TX, USA
M. Thomas , Dept. of Comput. Sci., Glasgow Univ., UK
J. Kelly , Loral SIS, Houston, TX, USA
M. Srivas , Collins Commercial Avionics, Rockwell Int. Corp., Cedar Rapids, IA, USA
pp. 30
Session 2

Inhibiting factors, market structure and the industrial uptake of formal methods (Abstract)

G. Cleland , Lab. for Found. of Comput. Sci., Edinburgh Univ., UK
D. MacKenzie , Lab. for Found. of Comput. Sci., Edinburgh Univ., UK
pp. 46

A C++ library for implementing specifications (Abstract)

D. Rann , Sch. of Comput., Staffordshire Univ., Stafford, UK
C. Minkowitz , Sch. of Comput., Staffordshire Univ., Stafford, UK
J.H. Turner , Sch. of Comput., Staffordshire Univ., Stafford, UK
pp. 61

Adding formal specifications to a proven V&V process for system-critical flight software (Abstract)

J.M. Bieman , Martin Marietta Astronaut. Co, Denver, CO, USA
J. Hagar , Martin Marietta Astronaut. Co, Denver, CO, USA
pp. 76
Session 3

Automatic verification of industrial designs (Abstract)

E.M. Clarke , Dept. of Eng. & Public Policy, Carnegie Mellon Univ., Pittsburgh, PA, USA
T. Kurfess , Dept. of Eng. & Public Policy, Carnegie Mellon Univ., Pittsburgh, PA, USA
V. Hartonas-Garmhausen , Dept. of Eng. & Public Policy, Carnegie Mellon Univ., Pittsburgh, PA, USA
D. Long , Dept. of Eng. & Public Policy, Carnegie Mellon Univ., Pittsburgh, PA, USA
pp. 88

Timing analysis of industrial real-time systems (Abstract)

S. Campos , Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
M. Minea , Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
W. Marrero , Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
E. Clarke , Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
pp. 97

Automated modular specification and verification of real-time reactive systems (Abstract)

J.S. Ostroff , Dept. of Comput. Sci., York Univ., North York, Ont., Canada
pp. 108

Formal validation of virtual finite state machines (Abstract)

M.G. Staskauskas , Dept. of Core Switching Dev., AT&T Bell Labs., Naperville, IL, USA
A.R. Flora-Holmquist , Dept. of Core Switching Dev., AT&T Bell Labs., Naperville, IL, USA
pp. 122
Session 4

A formal approach to reactive systems software: a telecommunications application in ESTEREL (Abstract)

C. Puchol , Dept. of Software Production Res., AT&T Bell Labs., Naperville, IL, USA
J.E. Von Olnhausen , Dept. of Software Production Res., AT&T Bell Labs., Naperville, IL, USA
L.J. Jagadeesan , Dept. of Software Production Res., AT&T Bell Labs., Naperville, IL, USA
pp. 132

A calculus of hazard for railway signalling (Abstract)

D.J. Mee , British Rail Res., Derby, UK
M. Ingleby , British Rail Res., Derby, UK
pp. 146

Experiences with specification and verification in LOTOS: a report on two case studies (Abstract)

M. Thomas , Dept. of Comput. Sci., Glasgow Univ., UK
C. Kirkwood , Dept. of Comput. Sci., Glasgow Univ., UK
pp. 159

Author Index (PDF)

pp. 172
98 ms
(Ver 3.1 (10032016))