GNOME: 
system specification and verification

A project of the Logic and Computation Group. 

GNOME is an object-oriented approach to the specification and verification of concurrent, reactive systems, including:

• a full fledged specification language supporting:
  • classes and inheritance;
  • encapsulation of attributes and methods;
  • object interaction via service invocation as well as through broadcasting of events;
  • concurrency between objects;
  • parameterized libraries.
• a linear temporal verification calculus supporting:
  • local reasoning within an object;
  • global reasoning within a community of possibly interacting objects;
  • proof of both safety and liveness properties.

The semantics of GNOME was initially provided axiomatically within a suitable linear temporal logic. Alternatives are currently being investigated using:

• object algebra, in cooperation with Aiguier and Bernot of the University of Evry in France;
• event structures;
• non-sequential automata;
• quantales;
• situation calculus;
• typed calculus of objects, in cooperation with Vasconcelos of the Faculty of Sciences of Lisbon.

Some relevant papers

• A. Ravara and V. Vasconcelos. Operational semantics and type system for Gnome on Typed Calculus of Objects. Presented at the ECOOP'96 Workshop on Proof-Theory of Concurrent Object-Oriented Programming.
  Get the paper: ps.gz.
   
• J. Ramos and A. Sernadas. A brief introduction to Gnome. Working paper, 1995.
  Get the paper: ps or dvi.
   
• P. Resende. Towards a Denotational Semantics of Imperative Objects. Presented at 11th ADT Workshop, Oslo, 1995.
   
• M. Aiguier, G. Bernot, J. Ramos, and A. Sernadas. An algebraic semantics for Gnome via a translation to Étoile Specifications. Presented at 11th ADT Workshop, Oslo, 1995.
  Get the paper: ps or dvi.
   
• C. Caleiro, G. Saake, and A. Sernadas. Deriving liveness goals from temporal logic specifications. Journal of Symbolic Computation 22:521-553, 1996.
  Get the paper: ps or dvi.
   
• P. Gouveia, R. Jungclaus, G. Saake, C. Sernadas. Feasible object certification. Research Report, 1995.
  Get the paper: ps or dvi.
   
• A. Sernadas, C. Sernadas and J. Ramos. A temporal logic approach to object certification. Journal Data and Knowledge Engineering, 19:267-294, 1996.
  Get the paper: ps or dvi.
   
• A. Sernadas, C. Sernadas, and J. F. Costa. Object specification logic. Journal of Logic and Computation, 5(5):603-630, 1995.
  Get the paper: ps or dvi.
   
• P. Gouveia, C. Sernadas. Enriching temporal object specification by abduction. Poster presented at 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 1995.
  Get the paper: ps or dvi.
   
• H.-D. Ehrich and A. Sernadas. Local specification of distributed families of sequential objects. In E. Astesiano, G. Reggio, and A. Tarlecki, editors, Recent Trends in Data Type Specification, pages 219-235, LNCS 906, Springer-Verlag, 1995.
  Get the paper: ps.Z.
   
• G. Saake, A. Sernadas, and C. Sernadas. Evolving object specifications. In R. Wieringa and R. Feemstra, editors, Information Systems: Correctness and Reusability (Selected Papers from the IS-CORE Workshop), pages 84-99, World Scientific, 1995.
  Get the paper: ps.gz.
   
• C. Caleiro. On the relationship between operational and denotational semantics of temporal logic specification of object behaviour. In R. Wieringa and R. Feemstra, editors, Information Systems: Correctness and Reusability (Selected Papers from the IS-CORE Workshop), pages 69-83, World Scientific, 1995.
  Get the paper: ps or dvi.
   
• P. Gouveia, C. Sernadas. Introducing explanations in temporal object specification. In R. Wieringa and R. Feemstra, editors, Information Systems: Correctness and Reusability (Selected Papers from the IS-CORE Workshop), pages 53-68, World Scientific, 1995.
  Get the paper: ps or dvi.
   
• A. Sernadas and C. Sernadas. Object certification. Presented at DAISD'94 and IS-CORE'94 Workshops, 1994.
  Get the paper: ps or dvi.
   
• H.-D. Ehrich, G. Denker, and A. Sernadas. Constructing systems as object communities. In M. C. Gaudel and J.-P. Jouannaud, editors, TAPSOFT'93, pages 453-467, LNCS 668, Springer-Verlag, 1993.
  Get the paper: ps.

For other relevant publications, you can browse the repository of publications of the Logic and Computation Group. 

Last update: March 5, 1998.