טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
Ph.D Thesis
Ph.D StudentSihman Marcelo
SubjectLanguage and Proof Support for Superimpositions and
Aspects
DepartmentDepartment of Computer Science
Supervisor Professor Shmuel Katz


Abstract

A `classic' distributed superimposition is a program module that can augment an underlying distributed program with added functionality, while cutting across usual language modularity constructs like processes, packages, or objects. The ideas of a `classic' distributed superimposition are used to design a new object-oriented version incorporating aspects, where a superimposition is a collection of generic parameterized aspects and new classes. The proposed construct extends the expressiveness and modularity of aspect-oriented programming (AOP). Among the new facilities proposed are: grouping related aspects into a superimposition, extending parameterization of aspects, dealing with interaction and interference among aspects, combining superimpositions to obtain new superimpositions, and proving correctness of a superimposition with aspects, like the validation of applications of aspects and superimpositions. New verification aspects and superimpositions are defined to modularize the proofs, and separate the proof-related code from the program and the aspects. This allows generating and activating a series of model checking tasks automatically each time a superimposition is applied to a basic program, achieving superimposition validation. Two ways of combining superimpositions to create new superimpositions are presented. In sequential combinations a new superimposition is obtained that is equivalent to first applying one, and then applying the second to the result. In merging combinations, it is as if each component superimposition is applied independently to a basic program, without mutual influences. Superimpositions are separately declared, specified, and verified. Among the examples used to demonstrate the approach are versions of the dining philosopher algorithm, a termination detection algorithm for distributed systems, and a monitoring superimposition that gathers statistics on basic objects.