Title page for E-project-031609-013504

Project Type MQP

Submission date 2009-03-16

Author
Theophilos John Giannakopoulos, CS

URN E-project-031609-013504

Title Towards a Transition System Semantics for Alloy

Advisor
Dougherty, Daniel J., CS

Availability unrestricted

Abstract
Alloy is a language for modeling systems using first order logic and relational algebra. In this paper we examine the use of Alloy for creating models of stateful systems, and we explore semantics for Alloy that define transition systems over database instances based on Alloy specifications written in the state-signature idiom. One such semantics is fully adequate for the original semantics of Alloy. We prove an undecidability result concerning the automatic synthesis of programs from specifications under this semantics.

Files
tgiannak-mqp.pdf

Browse by Author | Browse by Department | Search all available E-projects

Questions? Email project-questions@wpi.edu
Maintained by webmaster@wpi.edu

Project Type	MQP
Submission date	2009-03-16
Author	Theophilos John Giannakopoulos, CS
URN	E-project-031609-013504
Title	Towards a Transition System Semantics for Alloy
Advisor	Dougherty, Daniel J., CS
Availability	unrestricted
Abstract Alloy is a language for modeling systems using first order logic and relational algebra. In this paper we examine the use of Alloy for creating models of stateful systems, and we explore semantics for Alloy that define transition systems over database instances based on Alloy specifications written in the state-signature idiom. One such semantics is fully adequate for the original semantics of Alloy. We prove an undecidability result concerning the automatic synthesis of programs from specifications under this semantics.
Files	tgiannak-mqp.pdf