GPS/GIS와 RFID는 유비쿼터스 시대로 가는 우리 사회의 패러다임을 변화시켰다. 특히, 이러한 환경에서 지리적으로 분산되어 있고 운송해야 할 대상이 있는 이동 에이전트들은 자동으로 인식하고 추적할 수 있어야 한다. 그렇게 하기 위해서, 지리적 공간에서 에이전트들의 공간적/시간적 행위들을 명세하고 검증하기 위한 기본적인 이론과 기술들이 필요하다. 본 논문은 이를 위해 CaRDMI라는 새로운 정형기법을 제안한다. 명세를 위해 CaRDMI는 지도와 운송대상을 가지는 이동 에이전트들을 정의한다. 에이전트의 이동은 지도상의 경로로 표현되고 이들은 공간적/시간적 제약이 있는 노드와 에지들의 리스트들로 구성된다. 에이전트들 사이에서의 운송 대상에 관한 상호작용은 동기화 모드들에 의해 표현된다. 이들이 CaRDMI의 두드러진 특징이다. 특히, 시간 속성을 가진 다대다 동기화는 주목할만하다. CaRDMI는 분석과 검증을 위해 공간적, 시간적 그리고 상호작용을 위한 추론 규칙과 공간적/시간적 동일성 관계들을 제안한다.
GPS/GIS and RFID technologies have been changing the paradigm af our society toward ubiquitous era. Especially, geographically distributed mobile agents with transporting objects need to be automatically recognizable and traceable under certain conditions. To do this, fundamental theories and technologies are required to specify and verify spatial and temporal behaviors of agents on geographical space. This paper presents a new formal method, called Calculus of Real-Time Distribution, Mobility, and Interaction (CaRDMI), for this purpose. For specification, CaRDMI defines a map, mobile agents with transporting objects. The movement of on agent is represented by a path on the map, consisting of a list of nodes and a list of edges with spatial and temporal constraints. Interactive constraints among agents are represented by synchronization modes on objects at nodes. These constraints are distinguishable features of CaRDMI from other methods. Especially, many-to-many timed synchronization constraints are noticeable. For verification, CaRDMI presents the spatial, temporal and interactive deduction rules and the spatial and temporal equivalence relations.
