Software Engineering and Analysis Lab, IIIT-B
Formal Specificationf of Web apps using Statecharts
Statechart is an industry standard notation for describing life-cycles of important objects in a system. It is widely used in a variety of domains ranging from embedded to web-based enterprise software systems. A Statechart model is often large enough software artifact that it should come under the regular processes of quality assurance. Formal methods are mathematical techniques typically applied to verification and validation of systems. Formal methods have enjoyed signficant success and acceptance in the VLSI industry. In software, application domains bracketed as safety critical have embraced formal methods in their regular QA process in many cases. However, penetration of formal methods in other domains has been limited. The widely held perception that formal methods is hard to do plays an important role in this.
In this work, we intend to develop formal methods for general application domains. We have decided to use Statechart as the central element, which is a familiar notation to many software engineers. The technical work envisaged herein involves development of Statechart as a formal specification language, and development of algorithms to verify and validate the system both via static verification and automated testing. Formalisation of a well-known notation like Statechart will help wider acceptance in two ways. Firstly, it will help use of formal methods in a wider range of application domains. Secondly, it will make it accessible to a wider population of software engineers.