{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/76996"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/76996","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Ormolu : generating runtime monitors from alloy models","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Reeves, Dwayne Lloyd"],"institution":"Massachusetts Institute of Technology","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science.","school":null,"contributors":[],"advisors":["Daniel N. Jackson."],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011","date_published":"2011","updated_at":"2026-07-22T22:22:19Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"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."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/1721.1/76996","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Daniel N. Jackson."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science."]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science."]},{"key":"dc:creator","label":"Author","values":["Reeves, Dwayne Lloyd"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2013-02-14T15:36:25Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2013-02-14T15:36:25Z"]},{"key":"dc:date.issued","label":"Date","values":["2011"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Electrical Engineering and Computer Science."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["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."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/1721.1/76996"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis (M. Eng.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2011.","Cataloged from PDF version of thesis.","Includes bibliographical references (p. 57-58)."]},{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M.Eng."]},{"key":"dc:title","label":"Title","values":["Ormolu : generating runtime monitors from alloy models"]}]}],"canonical_facts":{"dc:contributor.advisor":["Daniel N. Jackson."],"dc:contributor.department":["Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science."],"dc:contributor.other":["Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science."],"dc:creator":["Reeves, Dwayne Lloyd"],"dc:date.accessioned":["2013-02-14T15:36:25Z"],"dc:date.available":["2013-02-14T15:36:25Z"],"dc:date.issued":["2011"],"dc:description":["Thesis (M. Eng.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2011.","Cataloged from PDF version of thesis.","Includes bibliographical references (p. 57-58)."],"dc:description.abstract":["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."],"dc:description.degree":["M.Eng."],"dc:identifier.uri":["http://hdl.handle.net/1721.1/76996"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"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."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["Ormolu : generating runtime monitors from alloy models"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:22:19Z"}