Tran, Sang Cong (1991) Applications of formal methods in engineering. PhD thesis, University of Warwick.

Preview

PDF WRAP_THESIS_Tran_1991.pdf - Submitted Version - Requires a PDF viewer. Download (53Mb) | Preview

Request Changes to record.

Abstract

The main idea presented in this thesis is to propose and justify a general framework for the development of safety-related systems based on a selection of criticality and the required level of integrity. We show that formal methods can be practically and consistently introduced into the system design lifecycle without incurring excessive development cost.
An insight into the process of generating and validating a formal specification from an engineering point of view is illustrated, in conjunction with formal definitions of specification models, safety criteria and risk assessments. Engineering specifications are classified into two main classes of systems, memoryless and memory bearing systems. Heuristic approaches for specification generation and validation of these systems are presented and discussed with a brief summary of currently available formal systems and their supporting tools.
It is further shown that to efficiently address different aspects of real-world problems, the concept of embedding one logic within another mechanised logic, in order to provide mechanical support for proofs and reasoning, is practical. A temporal logic framework, which is embedded in Higher Order Logic, is used to verify and validate the design of a real-time system. Formal definitions and properties of temporal operators are defined in HOL and real-time concepts such as timing marker, interrupt and timeout are presented. A second major case study is presented on the specification a solid model for mechanical parts. This work discusses the modelling theory with set theoretic topology and Boolean operations. The theory is used to specify the mechanical properties of large distribution transformers. Associated mechanical properties such as volumetric operations are also discussed.

Item Type:	Thesis (PhD)
Subjects:	Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Library of Congress Subject Headings (LCSH):	Formal methods (Computer science)
Official Date:	December 1991
Dates:	Date Event December 1991 Submitted
Institution:	University of Warwick
Theses Department:	School of Engineering
Thesis Type:	PhD
Publication Status:	Unpublished
Supervisor(s)/Advisor:	Hines, Evor, 1957-
Sponsors:	T&N Technology Ltd. ; Goodyear Transformers Ltd. ; Science and Engineering Research Council (Great Britain)
Extent:	2 v. (xiv, 344 leaves)
Language:	eng

Request changes or add full text files to a record

Repository staff actions (login required)

View Item

Downloads