Thread View: comp.specification
3 messages
3 total messages
Started by Chuck Howell
Tue, 29 May 1990 19:29
extracting spec of existing system
Author: Chuck Howell
Date: Tue, 29 May 1990 19:29
Date: Tue, 29 May 1990 19:29
24 lines
1635 bytes
1635 bytes
I've seen a few references here and there to using formal methods to specify an already implemented system; the claim is that this exercise was useful in identifying previously latent errors/ambiguities, and that the end product was a formal specification that corresponded pretty well with the implementations. I'm very interested in this approach, which seemingly is in the intersection of formal methods, reverse engineering/design recovery, and (corrective/perfective) maintenance. Any references, texts, anecdotes, etc. on this topic will be appreciated. If there's enough interest I'll post a summary to the net. Thanks a lot, Chuck -- +------------------------------------------------------------------------+ | Chuck Howell, M/S Z645 INTERNET: howell@community-chest.mitre.org | | The MITRE Corporation OR howell@mwunix.mitre.org | | 7525 Colshire Drive VOICE: (703) 883-6080 | | McLean VA 22102-3481 FAX: (703) 883-5519 | +------------------------------------------------------------------------+
Workshop on VDM application
Author: Cliff Jones
Date: Wed, 06 Jun 1990 08:49
Date: Wed, 06 Jun 1990 08:49
54 lines
2571 bytes
2571 bytes
A Case Study in Formal Methods THE WORKSHOP The increasing demand for high quality software has recently been underlined by the emergence of draft standards on safety related computer systems. In particular, the UK MoD Defence standard Def Stan 00-55 (Requirements for the Procurement of Safety Critical Software in Defence Equipment) mandates the use of formal methods and has focussed attention on what methodologies and tools can be used in the formal specification, development and verification of high integrity software. The purpose of the workshop is to give a simple but detailed example, especially for those with little knowledge of formal methods, which demonstrates some of the benefits to be obtained by using formal specifications. The case study to be discussed illustrates how a formal specification language (VDM) has been used to specify an international (ISO) banking standard which describes an approved message authenticator algorithm (MAA). Knowledge of VDM or the banking standard is not required. Comprehensive supporting documentation will be provided and there will be ample opportunity for discussion. The workshop will be presented by staff of the Software Engineering Group in NPL's Division of Information Technology and Computing, and by members of Program Validation Ltd. PROVISIONAL PROGRAMME 09.30 Registration and Coffee 10.00 Outline 10.15 Introduction to the MAA 10.45 Introduction to VDM 11.15 MAA in VDM 12.15 Discussion 12.30 Luncheon 13.45 Reassemble 14.00 Validation of the specification 14.30 Formal development of software 15.30 Tea 16.00 VDM tools 16.30 Discussion 17.00 Close For registration forms (or further information) please contact: G I Parkin (X7006, gip@seg.npl.co.uk) or G O'Neill (X7016, gon@seg.npl.co.uk) National Physical Laboratory, Teddington, Middlesex, TWLL 0LW. U.K. Telephone: 081 977 3222 (Switchboard) or 081 943 7006/7016.
Re: Workshop on VDM application ** MISSING DATE GIVEN **
Author: Cliff Jones
Date: Thu, 07 Jun 1990 10:36
Date: Thu, 07 Jun 1990 10:36
54 lines
2562 bytes
2562 bytes
A Case Study in Formal Methods THE WORKSHOP ** 10 July 1990 ** The increasing demand for high quality software has recently been underlined by the emergence of draft standards on safety related computer systems. In particular, the UK MoD Defence standard Def Stan 00-55 (Requirements for the Procurement of Safety Critical Software in Defence Equipment) mandates the use of formal methods and has focussed attention on what methodologies and tools can be used in the formal specification, development and verification of high integrity software. The purpose of the workshop is to give a simple but detailed example, especially for those with little knowledge of formal methods, which demonstrates some of the benefits to be obtained by using formal specifications. The case study to be discussed illustrates how a formal specification language (VDM) has been used to specify an international (ISO) banking standard which describes an approved message authenticator algorithm (MAA). Knowledge of VDM or the banking standard is not required. Comprehensive supporting documentation will be provided and there will be ample opportunity for discussion. The workshop will be presented by staff of the Software Engineering Group in NPL's Division of Information Technology and Computing, and by members of Program Validation Ltd. PROVISIONAL PROGRAMME 09.30 Registration and Coffee 10.00 Outline 10.15 Introduction to the MAA 10.45 Introduction to VDM 11.15 MAA in VDM 12.15 Discussion 12.30 Luncheon 13.45 Reassemble 14.00 Validation of the specification 14.30 Formal development of software 15.30 Tea 16.00 VDM tools 16.30 Discussion 17.00 Close For registration forms (or further information) please contact: G I Parkin (X7006, gip@seg.npl.co.uk) or G O'Neill (X7016, gon@seg.npl.co.uk) National Physical Laboratory, Teddington, Middlesex, TWLL 0LW. Telephone: 081 977 3222 (Switchboard) or 081 943 7006/7016.
Thread Navigation
This is a paginated view of messages in the thread with full content displayed inline.
Messages are displayed in chronological order, with the original post highlighted in green.
Use pagination controls to navigate through all messages in large threads.
Back to All Threads