UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Enhancing case tool support for analysis through formal logic utilities Borm, Eric A.


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.

Item Media

Item Citations and Data


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.