TRANSFORMATION OF AGGREGATE SPECIFICATIONS TO THE PREDICATE LOGIC MODELS


Henrikas Pranevicius, Regina Miseviciene, Vilius Misevicius, Business Informatics Department, Kaunas University of Technology, Studentu, 56,
E-mail: hepran@ktu.lt, regemise@ktu.lt, vilmise@ktu.lt

ABSTRACT: A paper deals with a transition from a formal aggregate specification to first order predicate logic clauses. Also this paper considers the analysis technique of general and individual properties of aggregate specifications using logic programming based language Prolog. The method is based on construction of formulae describing both aggregate specification and properties of the model under investigation. The resolution method implemented in Prolog is applied to generate a reach ability graph and to analyze it. Analysis of aggregate specifications for alternating bit protocol is presented.


KEYWORDS: Aggregate specification, predicate logic, Prolog, analysis

---

Back to HMS2003 Home Page