Summary: | 碩士 === 國立臺灣科技大學 === 工程技術研究所 === 81 === A systematic approach to verify timing constraints of software
system is presented. We extended the conventional ``Hoare-
logic'' with timing performance of software. For each software
control constructs some rules to reasoning timing performance
are derived and proposed. These rules can be used to reason
timing performance and to verify timing constraints by means of
foreward and backward operation, respectively. We also derived
the maximun and minimun execution time of software construct in
terms of concept of time interval. Hence, the attributes of
four special time points on time axis can be explored and
critical path of software system can be rigorously analyzed to
assist locating the trouble spots of timing performance. Our
approach can be associated with rapid prototyping development
method such that the timing constraints of software system can
be verified after specification stage. Therefore, redevelopment
of a software system caused by performance defect during
implementation can be avoided. A prototype hospital appointment
system is used to examplify the related concepts and techniques
in this paper.
|