Ormolu : generating runtime monitors from alloy models

This thesis presents Ormolu, a runtime monitor used for monitoring distributed systems. Given an Alloy model, Ormolu generates a database schema and translates the constraints of the model to queries over the database. The translation preserves the semantics of Alloy, especially in regards to its type system. Ormolu allows domain specific knowledge to be expressed in Alloy, where it can be checked and verified. The same model can then be used to check if the constraints of the model are still satisfied at runtime. The feasibility of Ormolu is examined in the domain of air traffic control at a local airport, using data provided by the Tower Flight Data Manager developed by Lincoln Laboratory.

Department dc:contributor.department

Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2011

Author dc:creator

• Reeves, Dwayne Lloyd

Advisor dc:contributor.advisor

• Daniel N. Jackson.

• Electrical Engineering and Computer Science.

Statement dc:rights

• M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/76996

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/76996