동적 시스템 명세를 위한 시제논리언어와 그 검증A Temporal Logic for Specification of Dynamic Systems and Its Verification

Cited 0 time in webofscience Cited 0 time in scopus
  • Hit : 468
  • Download : 267
DC FieldValueLanguage
dc.contributor.author조, 승모-
dc.contributor.author김, 형호-
dc.contributor.author차, 성덕-
dc.contributor.author배, 두환-
dc.contributor.authorCho, Seung-Mo-
dc.contributor.authorKim, Hyung-Ho-
dc.contributor.authorCha, Sung-Deok-
dc.contributor.authorBae, Doo-Hwan-
dc.date.accessioned2010-05-18T07:59:26Z-
dc.date.available2010-05-18T07:59:26Z-
dc.date.issued2002-
dc.identifier.citation정보과학회논문지 : 소프트웨어 및 응용, Vol.29, No.7, pp.450-464en
dc.identifier.issn1229-6848-
dc.identifier.urihttp://www.kiise.or.kr/-
dc.identifier.urihttp://hdl.handle.net/10203/18439-
dc.description.abstract대부분의 객체지향 시스템을 비롯한, 복잡한 시스템들은 그 구성요소들이 시스템의 수행시간 중에 변하는 동적인 특성을 가지고 있다. 하지만 대부분의 기존 분석기법들은 이러한 측면을 무시하고 있다. 이 논문에서는 이러한 동적 시스템을 명세하고 분석하기 위한 기법을 제안하고자 한다. 이를 위해, 동적 시스템의 명세를 기술하기 위한 새로운 시제논리인 HDTL을 제안하고, 기존의 시제논리를 위한 분석기법을 수정하여 새로운 tableau 기법을 제안하였다. HDTL은 변수와 한정자를 사용하여 동적 시스템의 자동적 분석을 가능하게 하였다. 이 기법을 사용하여 우리는 시스템의 요구사항 명세를 기술하고, 시스템의 수행이 그 명세를 만족하는지를 살펴 볼 수 있다 실험을 통해 HDTL과 분석기법의 적용성을 보였다en
dc.language.isokoen
dc.publisher한국정보과학회en
dc.subject정형적 명세en
dc.subject시제 논리en
dc.subject동적 시스템en
dc.subject테스팅en
dc.title동적 시스템 명세를 위한 시제논리언어와 그 검증en
dc.title.alternativeA Temporal Logic for Specification of Dynamic Systems and Its Verificationen
dc.typeArticleen
dc.description.alternativeAbstractMany modern complex systems, including most object-oriented systems, have dynamic characteristics that their components are dynamical]y configured during run-time. However, few analysis techniques are available that consider the dynamic nature of systems explicitly. We propose a specification and analysis method for these dynamic systems. We design a new temporal logic, called HDTL, to specify the properties of dynamically evolving systems, and tune up the tableau method for this logic. HDTL incorporates variables and quantifiers that enable the automatic analysis. Using HDTL and the analysis method, we can specify the correctness requirements of systems and check whether the system actually agree with the requirements or not. An experiment shows that HDTL is suitable for specifying dynamic properties and the analysis technique works well.en
dc.language.Alternativeen_USen
dc.subject.alternativeFormal Specificationen
dc.subject.alternativeTemporal Logicen
dc.subject.alternativeDynamic systemen
dc.subject.alternativeTestingen

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0