Model based verification of dynamically evolvable service oriented systems
Model based verification of dynamically evolvable service oriented systems
复制标题
动态演化的面向服务系统的基于模型的验证
DOI：
10.1007/s11432-015-5332-8
复制
发表时间：
2016-01
影响因子：
8.8
通讯作者：
Wu Weigang
中科院分区：
文献类型：
--
作者：
Zhou Yu;Ge Jidong;Zhang Pengcheng;Wu Weigang
动态演化是开放环境中面向服务系统的一个重要特征。为了使演化可信，保持过程与规范一致是至关重要的。在本文中，我们研究了两种演化场景，并提出了一种新的验证方法的基础上分层时间自动机模型检查与规范的一致性。它检查的过程之前，期间和之后的演变过程中，分别可以支持直接建模的时间方面，以及层次分解的软件结构。引入概率来模拟开放环境中的不确定性，从而可以支持参数级演化的验证。我们提出了一种扁平化算法，以促进使用主流的基于时间自动机的模型检查器UPPAAL（与UPPAAL-SMC集成）进行自动验证。我们还提供了一个激励性的例子与绩效评估，补充讨论，并证明了我们的方法的可行性。
Dynamic evolution is highly desirable for service oriented systems in open environments. For the evolution to be trusted, it is crucial to keep the process consistent with the specification. In this paper, we study two kinds of evolution scenarios and propose a novel verification approach based on hierarchical timed automata to model check the underlying consistency with the specification. It examines the procedures before, during and after the evolution process, respectively and can support the direct modeling of temporal aspects, as well as the hierarchical decomposition of software structures. Probabilities are introduced to model the uncertainty characterized in open environments and thus can support the verification of parameter-level evolution. We present a flattening algorithm to facilitate automated verification using the mainstream timed automata based model checker–UPPAAL (integrated with UPPAAL-SMC). We also provide a motivating example with performance evaluation that complements the discussion and demonstrates the feasibility of our approach.
登录
查看更多内容
DOI：
10.1016/j.jvlc.2005.11.001
发表时间：
2006-02
期刊：
J. Vis. Lang. Comput.
影响因子：
--
作者：
Karsten Hölscher;P. Ziemann;Martin Gogolla
通讯作者：
Karsten Hölscher;P. Ziemann;Martin Gogolla
环境驱动的Internetware软件模型
DOI：
10.1007/s11432-008-0057-6
发表时间：
2008-05
期刊：
Science in China(Series F:Information Sciences)
影响因子：
--
作者：
Ma XiaoXing;Huang Yu;Yu Ping;Lu Jian;Cao Chun;Tao XianPing
通讯作者：
Tao XianPing
DOI：
10.1109/qest.2009.41
发表时间：
2009-09
期刊：
2009 Sixth International Conference on the Quantitative Evaluation of Systems
影响因子：
--
作者：
A. Hartmanns;H. Hermanns
通讯作者：
A. Hartmanns;H. Hermanns
影响因子：
2.2
作者：
L. Baresi;E. D. Nitto;C. Ghezzi
通讯作者：
L. Baresi;E. D. Nitto;C. Ghezzi
影响因子：
7.4
作者：
Haibo Chen;Jie Yu;Chen Hang;B. Zang;P. Yew
通讯作者：
Haibo Chen;Jie Yu;Chen Hang;B. Zang;P. Yew