Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397
Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397
Issue N6 2015 year
As noted in the first part of the present article, methods of the formal verification are in the focus of scientific research since the 1960s. Such methods, however, still have to become an accepted part of software engineering verification toolbox. Approaches to the formal verification are usually divided into two distinct classes: model-theoretic and proof-theoretic. Model-theoretic approaches, most commonly referred as the model checking, are concerned with the extensive automatic check of some finitely describable model of the program states. Proof-theoretic, or deductive verification approaches, are focused on constructing proofs of target program desirable properties as derivations in a certain formal system. One of deductive verification branches having a lot of recent research activity is the dependently-typed programming. Based on informal observation of the intuitionistic natural deduction interpretability in terms of typed lambda-calculus, it is possible to create a proof-automation system using an expressive statically-typed functional programming language as its specification language. Formal semantics of both the general purpose and domain-specific programming languages can be described in terms of interpreters based on such a system. This representation may be utilized to simplify the process of the formal model elaboration for the software of interest.
The main contribution of the present article consists of literature review and critical analysis of the present state of research in the area of the formal verification, formal models of software and formally verifiable software development, based on the research results published in the time frame since 1990 to the present time. Publications on the listed topics are presented in a context of the software engineering development in general. The review is mainly concerned with the dependently-typed programming development and its application to the formal verification. Fundamental results associated with the main topic are also mentioned. In the conclusion possible directions of the further research is proposed. One of the mentioned further research areas of interest is the application of the formal verification to the language-oriented software engineering paradigm in form of domain-specific languages which have formal semantics defined by means of the generic dependently-typed intermediate representation.