All Outputs (3)

HighSpec: a Tool for Building and Checking OZTA Models (2006)
Conference Proceeding
Dong, J., Hao, P., Zhang, X., & Qin, S. (2006). HighSpec: a Tool for Building and Checking OZTA Models. In 28th International Conference on Software Engineering, 20-28 May 2006, Shanghai, China ; proceedings (775-778). https://doi.org/10.1145/1134409

HighSpec is an interactive system for composing and checking OZTA specifications. The integrated high level specification language, OZTA, is a combination of Object-Z (OZ) and Timed Automata (TA). Building on the strength of Object-Z's in specifying... Read More about HighSpec: a Tool for Building and Checking OZTA Models.

Integrating Probability with Time and Shared-Variable Concurrency (2006)
Conference Proceeding
Zhu, H., Qin, S., He, J., & Bowen, J. (2006). Integrating Probability with Time and Shared-Variable Concurrency. In 30th Annual IEEE/NASA Software Engineering Workshop, SEW-30, 24-28 April 2005, Columbia, Maryland ; proceedings (179-189). https://doi.org/10.1109/sew.2006.22

Complex software systems typically involve features like time, concurrency and probability, where probabilistic computations play an increasing role. It is challenging to formalize languages comprising all these features. In this paper, we integrate... Read More about Integrating Probability with Time and Shared-Variable Concurrency.

Constructing Property-Oriented Models for Verification (2006)
Conference Proceeding
He, J., Qin, S., & Sherif, A. (2006). Constructing Property-Oriented Models for Verification. In Unifying theories of programming : first international symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006 : revised selected papers (85-100). https://doi.org/10.1007/11768173_6

This paper advocates a general approach to formal verification by constructing property-oriented models. We instantiate the approach using timing properties, and construct a heterogeneous untimed model in which time is abstracted away, so that we can... Read More about Constructing Property-Oriented Models for Verification.