The stochastic semantics and verification for periodic control systems

Wang Z, Pu G, Qin S, et al. MDM: A mode diagram modeling framework for periodic control systems. The Computing Research Repository, 2012: abs/1207.0922. http://arxiv.org/abs/1207.0922

Cornelissen B, Zaidman A, Deursen A. A controlled experiment for program comprehension through trace visualization. IEEE Trans Softwe Eng, 2011, 37: 341–355

Liu N, Grundy J, Hosking J. A visual language and environment for composing web services. In: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering(ASE 2005), New York, 2005. 321–324

Dutertre B. Complete proof systems for first order interval temporal logic. In: Proceedings of the 1995 ACM/IEEE Symposium on Logic in Computer Science, San Diego, 1995. 36–43

Younes H, Simmons R. Probabilistic verification of discrete event systems using acceptance sampling. In: Proceedings of the 14th International Conference on Computer Aided Verification (CAV 2002), Copenhagen, 2002. 223–235

Younes H. Probabilistic verification for black-box systems. In: Proceedings of the 17th International Conference on Computer Aided Verification (CAV), Edinburgh, 2005. 253–265

Basu A, Bensalem S, Bozga M, et al. Statistical abstraction and model-checking of large heterogeneous systems. Int J Softw ToolTechnol Transf, 2012, 14: 53–72

David A, Larsen K, Legay A, et al. Time for statistical model checking of real-time systems. In: Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011), Snowbird, 2011. 349–355

Ching W, Michael K. Markov Chains: Models, Algorithms and Applications. New York: Springer-Verlag, 2005

Panangaden P. Labelled Markov Processes. London: Imperial College Press, 2010

Harel D. Statecharts: A visual formalism for complex systems. Sci Comput Program, 1987, 8: 231–274

Moszkowski B, Manna Z. Reasoning in interval temporal logic. In: Proceedings of International Workshop on Logics of Programs, pages 371–382, Carnegie Mellon University, Pittsburgh, PA, USA, June 6–8, 1983

Ball T, Majumdar R, Millstein T D, et al. Automatic predicate abstraction of c programs. In: Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2001), Snowbird, 2001. 203–213

Li L, Song X, Gu M, et al. Competent predicate abstraction in model checking. Sci China Inf Sci, 2011, 54: 258–267

Sen K, Viswanathan M, Agha G. Statistical model checking of black-box probabilistic systems. In: Proceedings of the 16th International Conference on Computer Aided Verification (CAV 2004), Boston, 2004. 202–215

Larsen K, Legay A, Traonouez L, et al. Robust specification of real time components. In: Proceedings of 9th International Conference of Formal Modeling and Analysis of Timed Systems(FORMATS), Aalborg, 2011

Harel D, Pnueli A. On the Development of Reactive Systems. New York: Springer-Verlag, 1985. 477–498

Giese H, Tichy M, Burmester S, et al. Towards the compositional verification of real-time UML designs. In: Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering (ESEC/FSE-11), New York, 2003. 38–47

Jahanian F, Mok A. Modechart: A specification language for real-time systems. IEEE Trans Softw Eng, 1994, 20: 933–947

Oh H, Ha S. Hardware-software cosynthesis of multi-mode multi-task embedded systems with real-time constraints. In: Proceedings of the 10th International Symposium on Hardware/Software Codesign (CODES 02), New York, 2002. 133–138

Schmitz M, Al-Hashimi B, Eles P. Cosynthesis of energy-efficient multimode embedded systems with consideration of mode-execution probabilities. IEEE Trans CAD Integr Circuits Syst, 2005, 24: 153–169

Henzinger T, Horowitz B, Kirsch C. Giotto: a time-triggered language for embedded programming. Technical report Department of Electronic Engineering and Computer Science University of California Berkeley CA USA. 2001

Kwiatkowska M, Norman G, Parker D. Prism 4.0: Verification of probabilistic real-time systems. In: Proceedings of the 2011 International Conference on Computer Aided Verification (CAV 2011), Snowbird, 2011. 585–591

Zheng Z, Ma S, Li W, et al. Complexity of software trustworthiness and its dynamical statistical analysis methods. Sci China Ser F-Inf Sci, 2009, 52: 1651–1657

Hartog J, Vink E. Verifying probabilistic programs using a hoare like logic. Int J Found Comput Sci, 2002, 13: 315–340

Stoddart B, Bell P. Probabilistic choice, reversibility, loops, and miracles. In: Proceedings of Third International Symposium on Unifying Theories of Programming(UTP 2010), Shanghai, 2010. 253–270