Formal Verification of the Accounting Information Interfaces Using Colored Petri Net

Abstract

In the process of Accounting Information System (AIS), the business transactions are generated by heterogeneous distributed applications. The business transactions result in T-accounts set up in the General Ledger System (GLS). The requirement changes maybe affect the screen scraping procedure of the business transactions interfaces, and also result in the issues of GLS process, system and control. In this paper, we propose a framework and alternative way to verify the business transaction interfaces of GLS in the early stage using the model checking technique. The GLS abstraction model are modeled using Colored Petri Net (CPN). Next, we verify the obtained CPN model using CPN tools to validate the GLS interfaces.