Information systems modeling: Language, verification, and tool support

Abstract

Information and processes are both important aspects of information systems. Nevertheless, most existing languages for modeling information systems focus either on one or the other. Languages that focus on information modeling often neglect the fact that information is manipulated by processes, while languages that focus on processes abstract from the structure of the information. In this paper, we present an approach for modeling and verification of information systems that combines information models and process models using an automated theorem prover. In our approach, set theory and first-order logic are used to express the structure and constraints of information, while Petri nets of a special kind, called Petri nets with identifiers, are used to capture the dynamic aspects of the systems. The proposed approach exhibits a unique balance between expressiveness and formal foundation, as it allows capturing a wide range of information systems, including infinite state systems, while allowing for automated verification, as it ensures the decidability of the reachability problem. The approach was implemented in a publicly available modeling and simulation tool and used in teaching of Information Systems students.