Accession Number : ADA265201


Title :   Formal Specification and Verification of Concurrent Programs


Descriptive Note : Final rept.


Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST


Personal Author(s) : Berry, Daniel M


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a265201.pdf


Report Date : Feb 1993


Pagination or Media Count : 108


Abstract : This module introduces formal specification of concurrent software and verification of the consistency between concurrent programs and their specifications. First, what one might want to be able to prove about a concurrent program is discussed. Then, a number of formal descriptions of the concept are presented. These vary in their coverage of the phenomena, and some can be used as the bases of formal specification of programs. Next, techniques for carrying out the proof of consistency between the specification and the program are described. Finally, it is noted that some of these techniques have automated tools such as verifiers associated with them.... Concurrent programs, Multiprocessing, Formal specification, Multitasking, Formal verification, Semantics of concurrency


Descriptors :   *SOFTWARE ENGINEERING , *COMPUTER PROGRAM VERIFICATION , COMPUTER PROGRAMS , DATA BASES , TOOLS , SEMANTICS , NUMBERS , THEOREMS , COMPUTER PROGRAM RELIABILITY , OPERATING SYSTEMS(COMPUTERS) , CONSISTENCY , COMPUTER PROGRAMMING , SPECIFICATIONS , ALGORITHMS


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE