|
Abstract: |
There are various approaches in developing software systems. In most of them, a specification is created before building the software. This approach avoids confusion at the later phase of software development. A simple way of writing the system specification is in the form of words (essay). Software engineer finds it difficult to infer the logics and behavior of the system under development (SUD) because writing gets very vague at times. To overcome this problem, Unified Modeling Language (UML) is used to provide a graphical notation for representing system's behavior. However UML model does not provide a formal approach for documenting specification and has a minimal support for the validation.
There are other ways of formally writing the system specification which can be verified using mathematical techniques and tools. Colored Petri-Nets is one of the formal specification techniques that can be used to model the system's behavior and check its correctness by analyzing liveness, boundedness, and deadlock properties [9]. Colored Petri Nets (CPN) can be modeled and analyzed using CPN Tools.
Thus before developing, software architect needs to create requirement specification in two formats. One format is to communicate with customers (like UML Sequence Diagram) and other format is for analysis and verification purpose (like Colored Petri Nets). An automated tool that can transform from UML like constructs to mathematical model such as Colored Petri-Nets might eliminate the redundancy of writing specification twice.
A Tool LSCTOCPN has been developed as a proof of concept which can be used to reduce the gap between informal method of software specification model and formal methods. This tool reads the Live Sequence Chart (LSC) Model of SUD as an input and transforms the system's behavior into a unified Colored Petri Nets (CPN) model. LSC is a Richer Construct than UML Sequence Diagram. The resulting CPN model of LSCTOCPN tool can be further analyzed using CPN Tools to identify whether the model satisfies the desired properties.
|
