Towards Using Formal Methods in Prototyping - Advantage or Impediment

Abstract

In aviation and other safety-critical domains, software faults are unacceptable. A means of detecting and avoiding these faults is to use formal methods. Although formal methods strongly contribute to the reliability and robustness of the system, some drawbacks prevent their general usage. A drawback is their reputation to be hard to apply for non-experts. Non-experts have to be familiarized with the tools to efficiently make use of them. But is this reputation still valid? Over the years, formal methods tools have evolved. They are capable to analyze more complex system properties. Further, their user experience was addressed by industrial companies to actually allow non-experts to profit from the advantages of formal methods. This paper represents the first step towards putting the mentioned assumption under test by trying to use formal methods for prototyping. We propose an approach for software prototyping which makes use of the formalization of requirements. We depict advantages and discuss first results of evaluating the commercial tool BTC EmbeddedPlatform R that we were able to use without cost in a project cooperation. We plan to continue the project cooperation to answer the headline in future.