An Algebraic Framework for Modeling of Mobile Systems(Concurrent Systems)
スポンサーリンク
概要
- 論文の詳細を見る
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.
- 社団法人電子情報通信学会の論文
- 2007-09-01
著者
-
Stefaneas Petros
School Of Applied Mathematical And Physical Sciences National Technical University Of Athens
-
OURANOS Iakovos
School of Electrical and Computer Engineering, National Technical University of Athens
-
FRANGOS Panayiotis
School of Electrical and Computer Engineering, National Technical University of Athens
-
Ouranos Iakovos
School Of Electrical And Computer Engineering National Technical University Of Athens
-
Frangos Panayiotis
School Of Electrical And Computer Engineering National Technical University Of Athens