SPIN Model Checker for MACT
Somavarapu, Murali Krishna
MetadataShow full item record
The SPIN (Simple PROMELA Interpreter) model checker is a verification system used to check high-level models of concurrent systems and improve the overall system’s performance. The SPIN model checker takes the PROMELA model as input and verifies the properties or system requirements to check for any errors in the system’s design based on the system requirements. The MACT (Model-based Aspect/Class Checking and Testing tool) has an excellent testing approach. The SPIN is added to the MACT to strengthen the results delivered by the MACT for a given aspect-oriented model. This paper discusses SPIN model implementation for the MACT tool and how SPIN technology is embedded into the MACT tool to check the syntax correctness of the state models. This paper also discusses the conversion of class models into PROMELA models and checks the design-level correctness of the PROMELA model in the MACT tool with respect to the system’s requirements.
Showing items related by title, author, creator and subject.
Lindgren, Christopher Aaron (2012-07-24)As the calendar turned over to 2012, an online learning initiative, Codecademy, declared it “Code Year”—the year “for everyone” to learn code. Within six months, this call has received much attention from the public and ...
Kolluru, Sunil (2014-08-04)Identity management is a key area for any enterprise. Maintaining user profiles, including e-mail, passwords, and other personal information, and providing a way to manage them is ubiquitous for any company. Specifically, ...
Application of the Kusumoto Cost-Metric to Evaluate the Cost-Effectiveness of Software Inspections Mandala, Narendar Reddy (2012-04-04)Inspection and testing are two widely recommended techniques for software quality improvement with a common goal of defect detection and removal in software products. While testing cannot be conducted until software is ...