Sciweavers

Share
ASWEC
2006
IEEE

Derivation of Java Monitors

9 years 2 months ago
Derivation of Java Monitors
This paper describes the formalisation of Java thread synchronisation in an extended Owicki-Gries theory, which facilitates the proof of safety and progress properties of multi-threaded Java programs. Although we can use this formalisation to verify existing Java programs, our focus is on deriving them instead. The derivation process consists of two stages: design and transformation. In the design stage, we use the method of Feijen and van Gasteren to obtain a program that satisfies the given requirements. This solution will most likely make atomicity assumptions Java is unable to guarantee. In the transformation stage, we reduce the granularity of the statements and develop a solution that can be translated directly to a Java implementation.
Brijesh Dongol
Added 10 Jun 2010
Updated 10 Jun 2010
Type Conference
Year 2006
Where ASWEC
Authors Brijesh Dongol
Comments (0)
books