NDSU North Dakota State University
Fargo, N.D.

NDSU Institutional Repository

SPIN Model Checker for MACT

Show simple item record

dc.description.abstract 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. en_US
dc.title SPIN Model Checker for MACT en_US
dc.date.accessioned 2013-12-12T17:13:29Z
dc.date.available 2013-12-12T17:13:29Z
dc.date.issued 2013-12-12
dc.identifier.uri http://hdl.handle.net/10365/23105
dc.subject SPIN (Computer file) en_US
dc.subject Computer software -- Verification. en_US
dc.subject Computer simulation -- Testing -- Data processing. en_US
dc.subject Modeling languages (Computer science). en_US
dc.subject Semantic computing.
dc.thesis.degree Paper (M.S.)-- North Dakota State University, 2013. en_US
dc.contributor.advisor Nygard, Kendall
dc.creator.author Somavarapu, Murali Krishna
dc.degree.departmentCollege Master of Science / Computer Science, College of Science and Mathematics, 2013.
dc.date.created 2013

This item appears in the following Collection(s)

Show simple item record

Search DSpace

Advanced Search


Your Account