Decentralized LTL Specifications for Ensuring Quality of Interaction-centralized System


KIPS Transactions on Software and Data Engineering, Vol. 3, No. 5, pp. 169-178, May. 2014
10.3745/KTSDE.2014.3.5.169,   PDF Download:

Abstract

In this paper, we present a research utilizing decentralized LTL specifications for ensuring a quality for interaction-centralizedsystem. In this system, for ensuring the quality, we need to validate interactions between modules of the system and then we shouldcheck whether the system achieves the expected requirements. This task remains difficult and labor-intensive and requires an expert.In this paper, we present a method to assist such a task. First of all, the requirements of the system is written as multiple LTLspecifications. Interactions between modules mean that behaviors of one module are related with other one``s behavior. We generate theautomaton model fully achieving specification through GR(1) synthesis. And we simulate them using the simulator based on thesoftware agent for checking behaviors of the system. Finally, we validate the whole system whether it achieves given requirements.


Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from September 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.


Cite this article
[IEEE Style]
R. K. Kwon and G. H. Kwon, "Decentralized LTL Specifications for Ensuring Quality of Interaction-centralized System," KIPS Transactions on Software and Data Engineering, vol. 3, no. 5, pp. 169-178, 2014. DOI: 10.3745/KTSDE.2014.3.5.169.

[ACM Style]
Ryoung Kwo Kwon and Gi Hwon Kwon. 2014. Decentralized LTL Specifications for Ensuring Quality of Interaction-centralized System. KIPS Transactions on Software and Data Engineering, 3, 5, (2014), 169-178. DOI: 10.3745/KTSDE.2014.3.5.169.