GTS-VL: 스마트 IoT에서 안전 요구사항 분석과검증을 위한 시각화 논리 언어 및 도구
GTS-Visual Logic: Visual Logic and Tool for Analysis and Verification of Secure Requirements in Smart IoT Systems
0
조회
0
다운로드
0
인용
0
참고문헌
키워드
초록
스마트 IoT의 특징인 분산성 및 이동성에 기반한 안전 요구사항을 분석 및 검증하기 위한 프로세스 대수 및 논리가 요구된다. 하지만 기존의프로세스 대수 및 논리는 분산성 및 이동성에 대한 표현이 제한적이므로 스마트 IoT의 요구사항 분석 및 검증이 비직관적이다. 이러한 한계를극복하기 위해, 본 논문에서는 GTS-VL(Geo-Temporal Space-Visual Logic)을 제시한다. GTS-VL은 GTS에서 표현된 블록 간의 관계를 다루는1차술어논리이며, GTS는 프로세스 대수인 dTP-Calculus를 사용하여 명세한 시스템의 동작 과정을 2차원 시공간에서 표현한 그래프이다. 본 논문에서 사용한 SAVE 도구는 ADOxx Meta-modeling Platform을 통해 개발되었으며, SAVE를 사용하여 PBC(Producer-Buffer-Consumer) 예제의 안전요구사항을 분석 및 검증하고 문자 및 시각화 기반 검증 방법을 비교 분석하여 장점 및 실용성을 보인다.
Abstract
It is necessary to apply process algebra and logic in order to analyze and verify safety requirements for Smart IoT Systems due todistributivity and mobility of the systems over some predefined geo-temporal space. However the analysis and verification cannot befully intuitive over the space due to the fact that the existing process algebra and logic are very limited to express the distributivityand the mobility. In order to overcome the limitations, the paper presents a new logic, namely for GTS-VL (Geo-Temporal Space-VisualLogic), visualization of the analysis and verification over the space. GTS-VL is the first order logic that deals with relations among thedifferent types of blocks over the space, which is the graph that visualizes the system behaviors specified with the existing dTP-Calculus. A tool, called SAVE, was developed over the ADOxx Meta-Modeling Platform in order to demonstrate the feasibility of the approach,and the advantages and practicality of the approach was shown with the comparative analysis of PBC (Producer-Buffer-Consumer) examplebetween the graphical analysis and verification method over the textual method with SAVE tool.
참고문헌 (17)
- K. Rob, "The real-time city? Big data and smart urbanism", GeoJournal, 79(1), pp.1~14 (2014)
- Y. Choe, "Process model to predict nondeterministic behavior of IoT systems", The 11th IFIP WG 8.1 working conference on the Practice of Enterprise Modelling (PoEM), pp.1~12 (2018)
- R. R. Smullyan, "First-order logic, Vol.43" (2012), Springer Science &Business Media
- L. Cardelli, "Mobile ambients", International Conference on Foundations of Software Science and Computation Structure, pp.140~155 (1998), Springer
- J. On, "A study on scheduler based on CARDMI process algebra for automated control of emergency medical system", Proceedings of the Korean Information Science Society Conference, pp.65~70 (2008), Korean Institute of Information Scientists and Engineers
- P. Coppin, "An attention based theory to explore affordances of textual and diagrammatic proofs", International Conference on Theory and Application of Diagrams (2010), Springer
- A. Shimojima, "An eye-tracking study of exploitations of spatial constraints in diagrammatic reasoning", International Conference on Theory and Application of Diagrams (2008), Springer
- D. H. Ballard, "Deictic codes for the embodiment of cognition", Behavioral and Brain Sciences, 20(4), pp.723~742 (1997)
- H. G. Fill, "On the conceptua-lisation of modeling methods using the ADOxx meta modeling platform", Enterprise Modeling and Information Systems Architectures (EMISAJ), 8, pp.4~25 (2013)
- E. M. Clarke, "Workshop on Logic of Programs", pp.52~71 (1981), Springer
- M. Huth, "Logic in computer science: Modelling and reasoning about systems" (2004), Cambridge University Press
- F. Jahanian, "Modechart: A specification language for real-time systems", IEEE Transactions on Software Engineering, 20, pp.933~947 (1994)
- A. G. Cohn, "Qualitative spatial representation and reasoning with the region connection calculus", GeoInformatica, 1(3), pp.275~316 (1993)
- A. U. Frank, "Qualitative spatial reasoning about distances and directions in geographic space", Journal of Visual Languages and Computing, 3(4), pp.343~371 (1992)
- D. Ladret, "VLP: A visual logic programming language", Journal of Visual Languages & Computing, 2(2), pp.163~188 (1991)
- V. Gervasi, "Complexity in Language and Text", pp.197~228 (2002)
- P. Coppin, "A cognitive exploration of the ‘non-visual’ nature of geometric proofs", Visual Languages and Logic, pp.81~95 (2009)