主 催: NII 先端ソフトウェア工学国際研究センター（GRACEセンター）
日 時：2008年6月25日（水）10:00-12:15
場 所：国立情報学研究所(NII) 20階 セミナー室１ (地図)
参加費：無料
お問い合わせ先：胡振江（Zhenjiang Hu） (hu _AT_ nii.ac.jp）
プログラム：
−Modelling and Verification of Mobile Systems using Pi-graphs
Frederic Peschanski (Pierre et Marie Curie University of Paris 6)
−Model Checking Mobility
Kenji Taguchi (GRACE Center, NII)
−Scalable management of heterogenous sensor data in dynamic environments
Levent Gurgen (Orange Labs)
▼プログラム
Modelling and Verification of Mobile Systems using Pi-graphs
Speaker:Frederic Peschanski (Pierre et Marie Curie University of Paris 6)
Abstract:This talk will introduce the pi-graphs, a new graphical model of mobile interactions that tries to accommodate the expressivity of the pi- calculus and the intuitiveness of place-transition nets. We give two complementary characterizations of pi-graphs. The first one relies on graph rewriting techniques. Complementarily, we develop a process-algebraic characterization : the pi-box calculus. We show that the two characterizations are equivalent, up-to structural congruence (i.e. graph isomorphism) and bisimilarity. An interesting characteristic of the model is its “locally synchronous, globally asynchronous” interpretation: each graph/term being attached to a clock evolving at the rate of interactions with the environment. This interpretation gives new opportunities for the efficient verification of mobile systems.
Biography: Frederic Peschanski is an assistant professor at UPMC Paris Universitas, France. He obtained his PhD from the same institution in 2002. He was in 2002-2004 a JSPS post-doctoral fellow at the Yonezawa laboratory, Tokyo University, working on mobile agent systems. His research interests include (but are not limited to) the integration of formal methods and techniques, the theory and practice of concurrent, disitributed and mobile systems, etc. Recently, he got particularily interested in graph rewriting systems.
Model Checking Mobility
Speaker:Kenji Taguchi (GRACE Center, NII)
Abstract: The notion of the mobile agents has been around for over a decade in order to capture the new form of computation in communication networks. As mobility is their inherent nature, it is hard to predict their behaviours before implementation. In this talk, I will give an overview of a formal notation for mobile agents called MobiOZ (Mobile Object-Z) and how to model check its specifications. The difficulty of verifying properties for mobile agent specifications is that agents are moving while exchanging messages locally and remotely. The basic idea of the verification method in this talk is to interpret mobility as state changes of a particular variable, which represents the current location for an agent instead of building a verifier based on the structural operational semantics of MobiOZ. MobiOZ specifications are translated into Promela, which is a process language for the SPIN model checker, and properties which include mobility and communication are proved by the SPIN. This is a joint work with Prof. J. S. Dong (National University of Singapore), which will appear in International Journal of Agent-Oriented Software Engineering (IJAOSE) : Special Issue on: Modelling Languages for Agent Systems.
Biography:Kenji Taguchi is a professor (by special appointment) at National Institute of Informatics (NII), Tokyo, Japan, which he joined in 2005. He has been working for an education program called “Top SE” led by Prof. Honiden since then. He holds PhD in Computer Science from Uppsala University, Sweden (2001). He was a lecturer at University of Bradford (UK), Uppsala University (Sweden), and a research associate at Kyushu University (Japan). Before he went into academia, He had worked in software industry for eleven years, mainly working for research and development of and consulting on AI systems such as expert systems, expert systems shells. His current research interests are a formal design notation for sensor networks, verification of large systems, application of security requirements methodologies to Common Criteria and BOK for formal methods. He has served on the PC member of several international conferences on software engineering and formal methods. He has jointly founded the Integrated Formal Methods Conference series in 1999.
Scalable management of heterogenous sensor data in dynamic environments
Speaker:Levent Gurgen (Orange Labs)
Abstract: Sensor data management has recently become a very active research domain. This presentation will introduce our work that deals with the issues related to scalable management of heterogeneous sensor data in dynamic environments. In fact, sensors are becoming cheaper, more and more numerous and heterogeneous. This naturally raises the problem of scalability and the need for integrating data collected from sensors with variable capabilities. Our work proposes a distributed and service-oriented architecture to tackle these issues. Data processing tasks are distributed at several levels in the architecture. Data management functionalities are provided in terms of services, in order to hide sensor heterogeneity behind generic services. The services implement our data and query model, SStreaM, which allows evaluating complex queries on heterogeneous sensor stream data.
This work equally introduces device management issues in sensor farms, a subject not yet explored in this context. It pertains to dealing with the management operations on sensors such as their configuration, software update or modification of their properties. These operations may be performed explicitly (e.g., by an administration console) or implicitly (e.g., consequence of autonomic management policy rules). These modifications should be taken into account dynamically by the sensor data management system. In fact, the management operations may modify the configuration of the system, therefore invalidate the results of continuous queries concurrently executing. This work proposes a concurrency control mechanism in order to deal with the conflicts which can manifest due to the concurrent execution of these operations.
The demonstration of our prototype SStreaMWare will conclude this presentation. SStreaMWare is a service oriented middleware for heterogeneous sensor data management. It provides a way of formulating declarative queries (via a graphical interface) on heterogeneous sensors such as temperature sensors, accelerometers, cameras, GPS devices, presence detectors, etc. Dynamic adaptation of the middleware against management operations will also be demonstrated.
※プログラムは予告なく変更される場合もありますのでご了承ください。
