Open Collections

Enhancing case tool support for analysis through formal logic utilities

University of British Columbia

Most support for analysis provided by current CASE (Computer Aided Software Engi neering) tools is complementary to the support provided by the tools being used to sup port formal methods; therefore, in order to provide more substantial support for analysis, CASE tools should be integrated with general purpose formal logic utilities, the tools of formal methods. Modern CASE tools are the product of many years of experience with developing software systems and provide a great deal of assistance with overcoming the organizational barriers to constructing large software systems. Unfortunately, the tools do not reflect the skills required to overcome the cognitive barriers faced by software engineers. Techniques of formal analysis provide solutions to overcoming some of those cognitive barriers. These techniques are based on formal logic and can only be applied within methodologies which make use of mathematically defined specification languages (i.e., formal methods). Computer assistance can be provided for these techniques of formal analysis through utilities which support formal logic such as model checkers and theorem provers. This dissertation proposes to combine the functionality of traditional CASE tools with utilities of formal logic. In support of this, a theorem prover for the formal logic, NaDSet, has been implemented in the commercial CASE tool, the Software Refinery.

Thesis/Dissertation

application/pdf

2009-03-04

For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.

http://hdl.handle.net/2429/5457

Computer Science

University of British Columbia

UBCV

DSpace