Extending the Theory of Owicki and Gries with a Logic of Progress

Dongol, Brijesh and Goldson, Doug (2005) Extending the Theory of Owicki and Gries with a Logic of Progress. Technical Report SSE-2005-03, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.

Document type: Department Technical Report
Collection: School of Information Technology and Electrical Engineering Publications
Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
LMCS.pdf LMCS.pdf application/pdf 850.51KB 172

Author Dongol, Brijesh
Goldson, Doug
Title Extending the Theory of Owicki and Gries with a Logic of Progress
School, Department or Centre Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering
Institution The University of Queensland
Report Number Technical Report SSE-2005-03
Publication date 2005-01-01
Subject 280302 Software Engineering
280300 Computer Software
280403 Logics and Meanings of Programs
280399 Computer Software not elsewhere classified
280402 Mathematical Logic and Formal Languages
280000 Information, Computing and Communication Sciences
Abstract/Summary This paper describes a logic of progress for concurrent programs. The logic is based on that of UNITY, molded to fit a sequential programming model. Integration of the two is achieved by using auxiliary variables in a systematic way that incorporates program counters into the program text. The rules for progress in UNITY are then modified to suit this new system. This modification is however subtle enough to allow the theory of Owicki and Gries to be used without change.
Keyword Owicki-Gries
Feijen-van Gasteren
UNITY
progress
formal methods
 
Versions
Version Filter Type
Access Statistics: 262 Abstract Views, 172 File Downloads  -  Detailed Statistics
Created: Fri, 12 Aug 2005, 10:00:00 EST by Brijesh Dongol  -  Detailed History