Formal analysis of IT systems requiremens

OData support
Dr. Pataricza András
Department of Measurement and Information Systems

The thesis aims at the elaboration of formal proofs of correctness of the joint specification of physical and business processes and controlled by information systems.

Requirement specification, as the first step of lifecycle design of information systems has a crucial effect on the success of the development. Traditional textual requirement specification become inadequate to substantiate complex systems, especially if they underlie extra-functional demands (e.g. security, performance…) in addition to functional ones. Therefore (semi-)formal modelling and its structuring of complex requirement systems and subsequent analysis by means of formal methods become more and more widely used.

Structuring of textual specifications is already supported in modern model-based requirement design paradigms by a variety of mathematical tools, moreover the academic world elaborated formal (e.g. ontology-based) methods for verifying the completeness and consistency of a model.

Nevertheless, until now, there are no available tools able to estimate the effect of a change in the functional requirements or in the environment. Engineering uses sensibility analysis in a variety of technical fields for similar problems, however it is not prevalent in IT systems engineering with the exception of a few specific fields.

The report adapts the concept of sensibility analysis for IT system design. There are two main types of system requirements: (i) Assumptions, which restrict the behavior of the operational environment and (ii) expectations to be granted by the designated system. For instance, a change in the environment (e.g. a new type of security attack unanticipated at the time of the elaboration of the system) may invalidate some assumptions, thus making the system vulnerable. Similarly, the set of expectations can alter or extended. Change impact analysis assessing the consequences of a local change propagating through the system necessitates a proper algorithmic support due to the huge number of possibilities.

My method generates exhaustively mutations corresponding to the effect of the possible changes. Critical changes and requirements affected by them can be estimated by means of sensibility analysis checking these mutations. This knowledge facilitates the further refinement of the system and the estimation of critical points to be reinforced.

The extensive analysis of the requirement model relies on a combination of different mathematical technics. The analysis can be automated by the specialization of general purpose formal methods-based tools to the problem. I developed a framework using the Alloy model-checker to implement sensibility analysis. This application also interfaces the Alloy sensibility analyzer and ontologies, which is used in industrial practice to store requirement systems.


Please sign in to download the files of this thesis.