@inproceedings{ca64c127920f47899a94dcc26b63ad46,
title = "Model checking real-time software system based on a new interface interaautomata with intense constrains",
abstract = "Components in software system usually interact with the environment by increasing complex interfaces to bring more possible failures with the increasing system scale, it has been becoming important to describe and verify the component properties by some formal methods at the interface level to guarantee its quality and reliability. Due to the weak or simplified multidimensional constraints specified between these different interfaces, the influence of performance, efficiency and sufficiency for the current interface automata based testing and verification is great, especially model checking with strict requirements of state space. To solve these challenges, we proposed a new defined interface interaction automata (IIA) to model the specification of the complex interaction process between input and output interfaces, including graphical value, temporal and real-time constraints. A transformation algorithm from interface interaction automata to timed automata model is designed, which can then be further model checked to verify the properties of the proposed IIA. SpaceWire bus protocol is selected as the experiment subject model checked based on the proposed model and methods to verify the feasibility and effectiveness.",
keywords = "I/O automata, interaction constraint, interface automata, model checking",
author = "Dongxiao Tang and Shunkun Yang",
note = "Publisher Copyright: {\textcopyright} 2015 IEEE.; 1st International Conference on Reliability Systems Engineering, ICRSE 2015 ; Conference date: 21-10-2015 Through 23-10-2015",
year = "2015",
month = dec,
day = "24",
doi = "10.1109/ICRSE.2015.7366476",
language = "英语",
series = "Proceedings of 2015 the 1st International Conference on Reliability Systems Engineering, ICRSE 2015",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
editor = "Shunong Zhang and Zili Wang",
booktitle = "Proceedings of 2015 the 1st International Conference on Reliability Systems Engineering, ICRSE 2015",
address = "美国",
}