An Algebraic Framework for Modeling of Mobile Systems

Panayiotis FRANGOS

IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E90-A    No.9    pp.1986-1999
Publication Date: 2007/09/01
Online ISSN: 1745-1337
DOI: 10.1093/ietfec/e90-a.9.1986
Print ISSN: 0916-8508
Type of Manuscript: PAPER
Category: Concurrent Systems
mobile computing,  algebraic specification,  formal verification,  observational transition systems,  CafeOBJ,  MobileOBJ,  

Full Text: PDF>>
Buy this Article

We present MobileOBJ, a formal framework for specifying and verifying mobile systems. Based on hidden algebra, the components of a mobile system are specified as behavioral objects or Observational Transition Systems, a kind of transition system, enriched with special action and observation operators related to the distinct characteristics of mobile computing systems. The whole system comes up as the concurrent composition of these components. The implementation of the abstract model is achieved using CafeOBJ, an executable, industrial strength algebraic specification language. The visualization of the specification can be done using CafeOBJ graphical notation. In addition, invariant and behavioral properties of mobile systems can be proved through theorem proving techniques, such as structural induction and coinduction that are fully supported by the CafeOBJ system. The application of the proposed framework is presented through the modeling of a mobile computing environment and the services that need to be supported by the former.