case study applications

Selected papers that describe applications of Alloy:

Papers on Teaching with Alloy

Teach foundational language principles

Communications of the ACM
Thomas Ball & Benjamin Zorn - 2015 - ACM

Using Alloy in Introductory Courses of Formal Methods

Structured Object-Oriented Formal Language and Method
Shin Nakajima - 2014 - Springer

Introducing Alloy in a Software Modelling Course

J Noble, DJ Pearce... - Formal Methods in Computer Science ..., 2008 - Citeseer

Chief Chefs of Z to Alloy: Using a Kitchen Example to Teach Alloy with Z

S Tarkan... - Teaching Formal Methods, 2009 - Springer

Workshop-modeling software the alloy way

MJ Lutz - Frontiers in Education Conference, 2008. FIE 2008. ..., 2008 -

A Lightweight Visual Approach to Teaching Formal Access Control Model for Computer Science Students

Z Chen... - and System (PACCS), 2011 Third Pacific- ..., 2011 -

Experiences of Teaching a Lightweight Formal Method

RC Boyatt... - Electronic Notes in Theoretical..., 2008 -

A Guide To Alloy

EYS Wong, M Herrmann... -

Experiences with Alloy in undergraduate formal methods

M Lutz - 2006 -

Enterprise Modeling

A model-driven environment for service design, simulation and prototyping

Exploring Services Science
Biljana Bajić-Bizumić & Claude Petitpierre & Hieu Chi Huynh et al. - 2013 - Springer

Simulation-Driven Approach for Business Rules Discovery

Advanced Information Systems Engineering Workshops
Biljana Bajić-Bizumić & Irina Rychkova & Alain Wegmann - 2013

Support for Domain Constraints in the Validation of Ontologically Well-Founded Conceptual Models

Enterprise, Business-Process and Information Systems Modeling
John Guerson & João Paulo A Almeida & Giancarlo Guizzardi - 2014 - Springer

Alloy4SPV: A Formal Framework for Software Process Verification

Modelling Foundations and Applications
Yoann Laurent & Reda Bendraou & Souheib Baarir et al. - 2014 - Springer

Debugging designs

14th International Workshop on High Performance Transaction Systems, Monterey
Chris Newcombe - 2011

Exploring the Alloy operational semantics for case management process modeling

Research Challenges in Information Science (RCIS), 2013 IEEE Seventh International Conference on
Irina Rychkova - 2013

An Example of a Hierarchical System Model Using SEAM and its Formalization in Alloy

A Wegmann, LS Le, I Rychkova... - ... Workshop, 2007. EDOC' ..., 2007 -


An Alloy Verification Model for Consensus-Based Auction Protocols

arXiv preprint arXiv:1407.5074
Saber Mirzaei & Flavio Esposito - 2014

Verifying dominant strategy equilibria in auctions

E Tadjouddine... - Multi-Agent Systems and Applications V, 2007 - Springer

Electronic Commerce

Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method

T Ramananandro - Formal Aspects of Computing, 2008 - Springer

An aspect oriented model of efficient and secure card-based payment system

DP Nigam... - Proceedings of the 2011 International Conference ..., 2011 -


Towards a formal foundation of web security

2010 23rd IEEE Computer Security Foundations Symposium
Devdatta Akhawe & Adam Barth & Peifung E. Lam et al. - 2010

The Same-Origin Policy

500 Lines or Less
Eunsuk Kang & Santiago Perez De Rosso & Daniel Jackson - 2016

Enforcing spatio-temporal access control in mobile applications

Ramadan Abdunabi & Wuliang Sun & Indrakshi Ray - 2014 - Springer

Toward a lightweight model of BGP safety

Proc. of WRiPE
Matvey Arye & Rob Harrison & Richard Wang et al. - 2011

Automated dynamic enforcement of synthesized security policies in android

Hamid Bagheri & Alireza Sadeghi & Reyhaneh Jabbarvand et al. - 2015

Network and Web Security Modeling and Analysis

Jason Bau - 2014

A Viewpoint-Based Approach for Formal Safety & Security Assessment of System Architectures

11th Workshop on Model-Driven Engineering, Verification and Validation
Julien Brunel & David Chemouil & Laurent Rioux et al. - 2014

Formal safety and security assessment of an avionic architecture with alloy

arXiv preprint arXiv:1405.1113
Julien Brunel & Laurent Rioux & Stéphane Paul et al. - 2014

Modeling and Verification of Redundancy Policies.

Hamza Chouh & Charlotte Callon & Ghita Jalal et al. - 2013

Formal model-based validation for tally systems

E-Voting and Identify
Dermot Cochran & Joseph R Kiniry - 2013 - Springer

Formalizing Security Aspects of the Web Platform in Alloy

Daniel Fett & Ralf Küsters - 2011

Model-driven approaches to analysing time-and location-dependent access control specifications

Emsaieb Mosbah Geepalla - 2013

Using model driven security approaches in web application development

Information and Communication Technology
Christoph Hochreiner & Zhendong Ma & Peter Kieseberg et al. - 2014 - Springer

Modeling Multiple Modes of Operation with Alloy

Computer Applications for Security, Control and System Engineering
Christos Kalyvas & Elisavet Konstantinou & Georgios Kambourakis - 2012 - Springer

A Lightweight Formal Approach for Analyzing Security of Web Protocols

Research in Attacks, Intrusions and Defenses
Apurva Kumar - 2014 - Springer

Managing trust and secrecy in identity management clouds

Proceedings of the 2012 ACM Workshop on Cloud computing security workshop
Apurva Kumar - 2012

Using automated model analysis for reasoning about security of web protocols

Proceedings of the 28th Annual Computer Security Applications Conference
Apurva Kumar - 2012

Security analysis of bytecode interpreters using alloy

Mark Clifford Reynolds & Assaf J Adviser-Kfoury - 2012 - Boston University

CORP: A Browser Policy to Mitigate Web Infiltration Attacks

Information Systems Security
Krishna Chaitanya Telikicherla & Venkatesh Choppella & Bruhadeshwar Bezawada - 2014 - Springer

Validation of a Security Model with the Alloy Analyzer

PS Grisham, CL Chen, S Khurshid... - 2008 -

Modeling partial attacks with Alloy

A Lin, M Bond... - Security Protocols, 2010 - Springer

Lightweight Modeling of Java Virtual Machine Security Constraints

M Reynolds - Abstract State Machines, Alloy, B and Z, 2010 - Springer

Using Lightweight Formal Methods for JavaScript Security

M Reynolds - 2010 -

A Lightweight Formal Analysis of a Multicast Key Management Scheme

D Jackson... - IFIP Lecture Notes in Computer Science (LNCS), 2011 -

Security Domain Model and Implementation Modeling

M Auguston, A Shaffer - 2008 -

Formal Models of a Least Privilege Separation Kernel in Alloy

M Auguston, TE Levin... - 2008 -

Toward a security domain model for static analysis and verification of information systems

A Shaffer - 2007 - DTIC Document

Access Control and Security Policies

Using i* to Model Access Policies: Relating Actors to Their Organizational Context

Social Modeling for Requirements Engineering
Robert Crook & Darrel Ince & Bashar Nuseibeh - 2011 - MIT Press

Early security patterns: A collection of constraints to describe regulatory security requirements

Requirements Patterns (RePa), 2012 IEEE Second International Workshop on
Robin A Gandhi & Mariam Rahmani - 2012

An Automated Approach to Detect Inconsistency and Semi-consistency Spatio-Temporal Role Based Access Control Specification

Journal of Data Processing
Emsaieb Geepalla & Behzad Bordbar - 2012

On formalizing of inconsistency and semi-consistency in spatio-temporal access control

Digital Information Management (ICDIM), 2012 Seventh International Conference on
Emsaieb Geepalla & Behzad Bordbar - 2012

Spatio-Temporal Role Based Access Control for Physical Access Control Systems

Emerging Security Technologies (EST), 2013 Fourth International Conference on
Emsaieb Geepalla & Behzad Bordbar & Xiaofeng Du - 2013

Transformation of spatio-temporal role based access control specification to alloy

Model and Data Engineering
Emsaieb Geepalla & Behzad Bordbar & Joel Last - 2012 - Springer

Role-Based Access Control modeling and validation.

Ramzi A Haraty & Mirna Naous - 2013

Assuring consistency in mixed models

Journal of Computational Science
Ramzi A Haraty & Mirna F Naous & Azzam Mourad - 2014 - Elsevier

Security analysis of temporal RBAC under an administrative model

Computers & Security
Sadhana Jha & Shamik Sural & Jaideep Vaidya et al. - 2014 - Elsevier

A Novel Trusted Hierarchy Construction for RFID-Sensor Based MANETs Using ECC

Electronics and Telecommunications Research Institute Journal
Adarsh Kumar & Krishna Gopal & Alok Aggarwal - 2014

Automatic conformance checking of role-based access control policies via alloy

Engineering Secure Software and Systems
David Power & Mark Slaymaker & Andrew Simpson - 2011 - Springer

Conformance checking of dynamic access control policies

Formal Methods and Software Engineering
David Power & Mark Slaymaker & Andrew Simpson - 2011 - Springer

Specification and Verification Using Alloy of Optimistic Access Control for Distributed Collaborative Editors

Formal Methods for Industrial Critical Systems
Aurel Randolph & Abdessamad Imine & Hanifa Boucheneb et al. - 2013 - Springer

Formal Verification of Cross-Domain Access Control Policies Using Model Checking

Mark C Reynolds & Azer Bestavros - 2011 - Citeseer

PCIEF: a policy conflict identification and evaluation framework

International Journal of Information and Computer Security
Vimalathithan Subramanian & Remzi Seker & Srini Ramaswamy et al. - 2012 - Inderscience

Rigorous analysis of uml access control policy models

Policies for Distributed Systems and Networks (POLICY),
2011 IEEE International Symposium on
Wuliang Sun & Robert France & Indrakshi Ray - 2011

Alloy model for Cross Origin Request Policy (CORP)

Krishna Chaitanya Telikicherla & Venkatesh Choppella - 2013

Using Automated Model Analysis for Reasoning about Security

Apurva Kumar - 2012 - IBM Research India

Rigorous Analysis of UML Access Control Policy Models

W Sun, R France... - Policies for Distributed Systems and ..., 2011 -

Automatic conformance checking of role-based access control policies via alloy

D Power, M Slaymaker... - Engineering Secure Software and ..., 2011 - Springer

Conformance checking of dynamic access control policies

D Power, M Slaymaker... - Formal Methods and Software ..., 2011 - Springer

Enabling verification and conformance testing for access control model

H Hu... - Proceedings of the 13th ACM Symposium on Access ..., 2008 -

Verification of policy-based self-managed cell interactions using alloy

A Schaeffer-Filho, E Lupu, M Sloman... - ... and Networks, 2009. ..., 2009 -

Ensuring spatio-temporal access control for real-world applications

M Toahchoodee, I Ray, K Anastasakis... - Proceedings of the 14th ..., 2009 -

Formal verification of OAuth 2.0 using Alloy framework

S Pai, Y Sharma, S Kumar... - ... Systems and Network ..., 2011 -

Conformance verification of privacy policies

X Fu - Web Services and Formal Methods, 2011 - Springer

Formalising and validating RBAC-to-XACML translation using lightweight formal methods

M Slaymaker, D Power... - Abstract State Machines, Alloy, B ..., 2010 - Springer

A Formal Method Based Case Study for Access Control

G Li, Y Xiao, M Lu... - Computational Intelligence and ..., 2009 -

On the modelling and analysis of Amazon Web Services access policies

D Power, A Simpson... - A Proof based approach ..., 2009 -

New Approach for Testing the Correctness of Access Control Policies

S Sharma... - 2009 -

An Application of Alloy to Static Analysis for Secure Information Flow and Verification of Software Systems

AB Shaffer - 2008 - DTIC Document

Feature Modeling and Analysis

Feature and meta-models in Clafer: mixed, specialized, and coupled

Software Language Engineering
Kacper Bąk & Krzysztof Czarnecki & Andrzej Wąsowski - 2011 - Springer

Supporting Multi-Level Configuration with Feature-Solution Graphs: Formal Semantics and Alloy implementation

Jaime Chavarriaga & Carlos Noguera & Rubby Casallas et al. - 2013

Translating the Feature-Oriented Requirements Modelling Language to Alloy

David Dietrich & Pourya Shaker & Jan Gorzny et al. - 2012

Pairwise testing for software product lines: comparison of two approaches

Software Quality Journal
Gilles Perrouin & Sebastian Oster & Sagar Sen et al. - 2012 - Springer

Feature and class models in Clafer: Mixed, specialized, and coupled

K Bak, K Czarnecki... - ... on Software Language ..., 2010 -

Detecting dependences and interactions in feature-oriented design

S Apel, W Scholz, C Lengauer... - ... (ISSRE), 2010 IEEE ..., 2010 -

Variability modeling and qos analysis of web services orchestrations

A Kattepur, S Sen, B Baudry... - Web Services (ICWS), ..., 2010 -

Domain Specific Languages and Modeling

Supervisory control theory with Alloy

Science of Computer Programming
Benoit Fraikin & Marc Frappier & Richard St-Denis - 2014 - Elsevier

Modeling the supervisory control theory with Alloy

Abstract State Machines, Alloy, B, VDM, and Z
Benoit Fraikin & Marc Frappier & Richard St-Denis - 2012 - Springer

Using alloy to support feature-based DSL construction for mining software repositories

Proceedings of the 17th International Software Product Line Conference co-located workshops
Changyun Huang & Yasutaka Kamei & Kazuhiro Yamashita et al. - 2013

$Rby—An Embedding of Alloy in Ruby

Abstract State Machines, Alloy, B, TLA, VDM, and Z
Aleksandar Milicevic & Ido Efrati & Daniel Jackson - 2014 - Springer

Verification of DSMLs using graph transformation: a case study with Alloy

Z Demirezen, M Mernik, J Gray... - ... Workshop on Model-Driven ..., 2009 -

Train Control

Specifying a Testing Oracle for Train Stations--Going beyond with Product Line Technology

Models in Software Engineering
Andreas Svendsen & Øystein Haugen & Birger Møller-Pedersen - 2012 - Springer

Specifying a testing oracle for train stations

Proceedings of the 8th International Workshop on Model-Driven Engineering, Verification and Validation
Andreas Svendsen & Øystein Haugen & Birger Møller-Pedersen - 2011

Model based specification validation for automatic train protection and block system

Computing and Convergence Technology (ICCCT), 2012 7th International Conference on
Guo Xie & Xinhong Hei & Hiroshi Mochizuki et al. - 2012

Formalizing train control language: automating analysis of train stations

A Svendsen, B Møller-Pedersen... - ... in Railways XII: ..., 2010 -

File systems

Formal modeling and analysis of a flash filesystem in Alloy

E Kang... - Abstract state machines, B and Z, 2008 - Springer

Variations on an Alloy-centric tool-chain in verifying a journaled file system model

MA Ferreira... - 2010 -

Verifying Intel flash file system core specification

MA Ferreira, SS Silva... - ... in VDM: Proceedings of the Fourth ..., 2008 -

Software Architecture

Towards formalizing assumptions on architectural level: A proof-of-concept

Abdullah Al Mamun & Matthias Tichy & Jörgen Hansson - 2012 - Departmen of Computer Science and Engineering

A Formal Approach for Incorporating Architectural Tactics into the Software Architecture.

Hamid Bagheri & Kevin J Sullivan - 2011

Efficient re-resolution of SMT specifications for evolving software architectures

Proceedings of the 10th international ACM Sigsoft conference on Quality of software architectures
Kenneth Johnson & Radu Calinescu - 2014

CD2Alloy: Class diagrams analysis using Alloy revisited

Model Driven Engineering Languages and Systems
Shahar Maoz & Jan Oliver Ringert & Bernhard Rumpe - 2011 - Springer

Analyzing variability: capturing semantic Ripple effects

Modelling Foundations and Applications
Andreas Svendsen & Øystein Haugen & Birger Møller-Pedersen - 2011 - Springer

A Lightweight Modeling and Verifying Method for Dynamic Evolution of Software Architectures Using Alloy.

Journal of Convergence Information Technology
Hongzhen Xu & Guosun Zeng - 2013

Model checking software architecture design

High-Assurance Systems Engineering (HASE), 2012 IEEE 14th International Symposium on
Jiexin Zhang & Yang Liu & Jing Sun et al. - 2012

Monarch: Model-based development of software architectures

H Bagheri, K Sullivan - Model Driven Engineering Languages and ..., 2010 - Springer

Dynamic software architectures verification using DynAlloy

A Bucchiarone... - Electronic Communications of ..., 2008 -

A formal specification of the Fractal component model in Alloy

P Merle, JB Stefani - 2008 -

Assessing Component's Behavioral Interoperability Concerning Goals

W Ma, L Chung... - On the Move to Meaningful Internet Systems: ..., 2008 - Springer

A middleware model in alloy for supply chain-wide agent interactions

R Haesevoets, D Weyns, M Cruz Torres... - Agent-Oriented ..., 2011 - Springer

Modeling and analyzing architectural change with alloy

KM Hansen... - Proceedings of the 2010 ACM Symposium on ..., 2010 -

Modeling and analysis of Reo connectors using Alloy

R Khosravi, M Sirjani, N Asoudeh, S Sahebi... - ... Models and Languages, 2008 - Springer

Graph-based design and analysis of dynamic software architectures

R Bruni, A Bucchiarone, S Gnesi, D Hirsch... - ... , Graphs and Models, 2008 - Springer

Towards self-management in service-oriented computing with modes

H Foster, S Uchitel, J Kramer... - Service-Oriented Computing- ..., 2009 - Springer

Dynamic software architectures for global computing systems

A Bucchiarone - 2008 -

A model transformation approach to derive architectural models from goal-oriented requirements models

M Lucena, J Castro, C Silva, F Alencar... - On the Move to ..., 2009 - Springer

Specifying Self-configurable Component-Based Systems with FracToy

A Tiberghien, P Merle... - Abstract State Machines, Alloy, B ..., 2010 - Springer

Analyzing architectural styles

JS Kim... - Journal of Systems and Software, 2010 - Elsevier

Verification of replication architectures in AADL

D de Niz... - Engineering of Complex Computer ..., 2009 -

Architectural style as an independent variable

H Bagheri, Y Song... - Proceedings of the IEEE/ACM ..., 2010 -


Synchronizing model and program refactoring

Formal methods: foundations and applications
Tiago Massoni & Rohit Gheyi & Paulo Borba - 2011 - Springer

UML model refactoring: a systematic literature review

Empirical Software Engineering
Mohammed Misbhauddin & Mohammad Alshayeb - 2013 - Springer

Automated behavioral testing of refactoring engines

Software Engineering, IEEE Transactions on
Gustavo Soares & Rohit Gheyi & Tiago Massoni - 2013 - IEEE

Identifying overly strong conditions in refactoring implementations

Software Maintenance (ICSM), 2011 27th IEEE International Conference on
Gustavo Soares & Melina Mongiovi & Rohit Gheyi - 2011

Analyzing Behavioral Refactoring of Class Models.

Wuliang Sun & Robert B France & Indrakshi Ray - 2013

Alloy as a Refactoring Checker?

H Estler, H Wehrheim - Electronic Notes in Theoretical Computer ..., 2008 - Elsevier

Sound Object Model Refactorings

R Gheyi... - 2010 -

Toward a Formal Evaluation of Refactorings

J Paul, N Kuzmina, R Gamboa... - Formal Methods ..., 2008 -

Formal model-driven program refactoring

T Massoni, R Gheyi... - Proceedings of the Theory and practice ..., 2008 -

Synchronizing model and program refactoring

T Massoni, R Gheyi... - Formal Methods: Foundations and ..., 2011 - Springer

Program verification

Verification of i* models using alloy

Information Systems Development
Peter Oluoch Ating’a & Aneesh Krishna - 2011 - Springer

Verification of ATL transformations using transformation models and model finders

Formal Methods and Software Engineering
Fabian Büttner & Marina Egea & Jordi Cabot et al. - 2012 - Springer

Optimized translation of clafer models to alloy

Kacper Bak - 2011

SEFM: software engineering and formal methods

Software & Systems Modeling
Gilles Barthe & Alberto Pardo & Gerardo Schneider - 2014 - Springer

Data Model Bugs

NASA Formal Methods
Ivan Bocić & Tevfik Bultan - 2015 - Springer

Automated specification analysis using an interactive theorem prover

Formal Methods in Computer-Aided Design (FMCAD), 2011
Harsh Raju Chamarthi & Panagiotis Manolios - 2011

Practical JFSL verification using TACO

Software: Practice and Experience
M Chicote & Daniel Ciolek & Juan Pablo Galeotti - 2014 - Wiley Online Library

Model checking support for conflict resolution in multiple non-functional concern management

Euro-Par 2011: Parallel Processing Workshops
Marco Danelutto & Peter Kilpatrick & Carlo Montangero et al. - 2012

Empirical comparison and performance evaluation of adequacy criteria for testing database application

Jitendra D Deshmukh - 2012 - Jhunjhunu

Relational reasoning via SMT solving

FM 2011: Formal Methods
Aboubakr Achraf El Ghazi & Mana Taghdiri - 2011 - Springer

Specifying UML protocol state machines in Alloy

Integrated Formal Methods
Ana Garis & Ana CR Paiva & Alcino Cunha et al. - 2012

A dual-engine for early analysis of critical systems

arXiv preprint arXiv:1408.0707
Aboubakr Achraf El Ghazi & Ulrich Geilmann & Mattias Ulbrich et al. - 2014

Behavioral validation of JFSL specifications through model synthesis

Proceedings of the 34th International Conference on Software Engineering
Carlo Ghezzi & Andrea Mocci - 2012

Checking Transformation Model Properties with a UML and OCL Model Validator

Proc. 3rd Int. STAF’2014 Workshop Verification of Model Transformations (VOLT’2014)
Martin Gogolla & Lars Hamann & Frank Hilken - 2014

Generating JML Specifications from Alloy Expressions

Hardware and Software: Verification and Testing
Daniel Grunwald & Christoph Gladisch & Tianhai Liu et al. - 2014 - Springer

Formalization of fUML: An Application to Process Verification

Advanced Information Systems Engineering
Yoann Laurent & Reda Bendraou & Souheib Baarir et al. - 2014

Formal verification of Pastry using TLA+

International Workshop on the TLA+ Method and Tools
Tianxiang Lu & Stephan Merz & Christoph Weidenbach - 2012

Symbolic execution for (almost) free: Hijacking an existing implementation to perform symbolic execution

Joseph P Near & Daniel Jackson - 2014

Rubicon: bounded verification of web applications

Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering
Joseph P Near & Daniel Jackson - 2012

How Amazon web services uses formal methods

Communications of the ACM
Chris Newcombe & Tim Rath & Fan Zhang et al. - 2015 - ACM

An integrated data model verifier with property templates

Formal Methods in Software Engineering (FormaliSE), 2013 1st FME Workshop on
Jaideep Nijjar & Ivan Bocic & Tevfik Bultan - 2013

Unbounded data model verification using SMT solvers

Automated Software Engineering (ASE), 2012 Proceedings of the 27th IEEE/ACM International Conference on
Jaideep Nijjar & Tevfik Bultan - 2012

Alloy meets the algebra of programming: A case study

Software Engineering, IEEE Transactions on
Jose N Oliveira & Miguel A Ferreira - 2013 - IEEE

A dataflow analysis to improve sat-based bounded program verification

Software Engineering and Formal Methods
Bruno Cuervo Parrino & Juan Pablo Galeotti & Diego Garbervetsky et al. - 2011 - Springer

OCL-Lite: Finite reasoning on UML/OCL conceptual schemas

Data & Knowledge Engineering
Anna Queralt & Alessandro Artale & Diego Calvanese et al. - 2012 - Elsevier

Modeling the Java Bytecode Verifier

Science of Computer Programming
Mark C Reynolds - 2013 - Elsevier

Parallel bounded analysis in code with rich invariants by refinement of field bounds

Proceedings of the 2013 International Symposium on Software Testing and Analysis
Nicolás Rosner & Juan Galeotti & Santiago Bermúdez et al. - 2013

Finding errors from reverse-engineered equality models using a constraint solver

Software Maintenance (ICSM), 2012 28th IEEE International Conference on
Chandan Raj Rupakheti & Daqing Hou - 2012

Towards a methodology for verifying partial model refinements

Software Testing, Verification and Validation (ICST), 2012 IEEE Fifth International Conference on
Rick Salay & Marsha Chechik & Jan Gorzny - 2012

Model transformation specification for automated formal verification

Software Engineering (MySEC), 2011 5th Malaysian Conference in
Asmiza Abdul Sani & Fiona AC Polack & Richard F Paige - 2011

Trans-DV: A Framework for Developing and Formally Verifying Model Transformation Specifications

Sponsoring Institutions
Asmiza A Sani & Fiona AC Polack & Richard F Paige - 2011

Specification and Verification of Graph-Based Model Transformation Properties

Graph Transformation
Gehan MK Selim & Levi Lúcio & James R Cordy et al. - 2014 - Springer

A feedback technique for unsatisfiable UML/OCL class diagrams

Software: Practice and Experience
Asadullah Shaikh & Uffe Kock Wiil - 2014 - Wiley Online Library

Analyzing temporal properties of abstract models

Proceedings of the 2011 26th IEEE/ACM International Conference on Automated Software Engineering
Amirhossein Vakili - 2011

Reducing CTL-live Model Checking to First-Order Logic Validity Checking

Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design
Amirhossein Vakili & Nancy A Day - 2014

Verification of model transformations using Alloy

PAMT 2014
Xiaoliang Wang - 2014

Scalable Verification of Model Transformations

11th Workshop on Model Driven Engineering, Verification and Validation MoDeVVa 2014
Xiaoliang Wang & Adrian Rutle & Yngve Lamo - 2014

How To Make Chord Correct

Pamela Zave - 2014

Verifying specifications with associated attributes in graph transformation systems

Frontiers of Computer Science
Yu Zhou & Yankai Huang & Ou Wei et al. - 2015 - Springer

Equals Checker (EQ)

CR Rupakheti... - 2011 -

A Security Domain Model for Static Analysis and Verification of Software Programs

AB Shaffer, M Auguston, C Irvine... - Proceedings of the 20th ..., 2008 -

Analyzing Ruby on Rails Data Models using Alloy

J Nijjar... - GSWC 2010, 2010 -

Analysis of invariants for efficient bounded verification

JP Galeotti, N Rosner, CG Lopez Pombo... - Proceedings of the 19th ..., 2010 -

Automatic code generation and solution estimate for object-oriented embedded software

RR Ferreira - Companion to the 23rd ACM SIGPLAN conference on ..., 2008 -

Formal Logic Based Configuration Modeling and Verification for Dynamic Component Systems

Z Theisz, G Batori... - MOPAS 2011, The Second ..., 2011 -

An Abstraction-Oriented, Path-Based Approach for Analyzing Object Equality in Java

CR Rupakheti... - Reverse Engineering (WCRE), 2010 ..., 2010 -


Systematic testing of database engines using a relational constraint solver

Software Testing, Verification and Validation (ICST), 2011 IEEE Fourth International Conference on
Shadi Abdul Khalek & Sarfraz Khurshid - 2011

Bounded verification of Ruby on Rails data models

Proceedings of the 2011 International Symposium on Software Testing and Analysis
Jaideep Nijjar & Tevfik Bultan - 2011

A Framework for Verifying Consistency of SQL-DB Ontology using Alloy

한국정보과학회 학술발표논문집
Isma Farah Siddiqui & Scott Uk-Jin Lee - 2014

Mapping between Alloy specifications and database implementations

A Cunha... - Software Engineering and Formal ..., 2009 -

Towards an Alloy Formal Model for Flexible Advanced Transactional Model Development

B Gallina, N Guelfi... - ... Engineering Workshop (SEW), ..., 2009 -

Model-driven Development

Automated Composition of Sequence Diagrams via Alloy.

Mohammed Alwanain & Behzad Bordbar & Juliana Küster Filipe Bowles - 2014

A model driven approach to analysis and synthesis of sequence diagrams

Mohamed Ariff Ameedeen - 2012

Bottom-up model-driven development

Software Engineering (ICSE), 2013 35th International Conference on
Hamid Bagheri & Kevin Sullivan - 2013

Metamodel based methodology for dynamic component systems

Modelling Foundations and Applications
Gabor Batori & Zoltan Theisz & Domonkos Asztalos - 2012 - Springer

Translating between Alloy specifications and UML class diagrams annotated with OCL

Software & Systems Modeling
Alcino Cunha & Ana Garis & Daniel Riesco - 2013 - Springer

Automatic Unbounded Verification of Alloy Specifications with Prover9

Alcino Cunha & Nuno Macedo - 2011

Supporting model based design

Model and Data Engineering
Rémi Delmas & David Doose & Anthony Fernandes Pires et al. - 2011 - Springer

A verification and validation process for model-driven engineering

Progress in Flight dynamics, guidance, navigation,
control, fault detection, and avionics
Rémi Delmas & A Fernandes Pires & Thomas Polacsek - 2013

Combining formal verification environments and model-driven engineering

Selma Djeddai - 2013

Chaining model transformations

Proceedings of the First Workshop on the Analysis of Model Transformations
Anne Etien & Vincent Aranega & Xavier Blanc et al. - 2012

ConceVE: Conceptual modeling and formal validation for everyone

ACM Transactions on Modeling and Computer Simulation
Ross Gore & Saikou Diallo & Jose Padilla - 2014 - ACM

Lightweight formalization and validation of ORM models

Journal of Logical and Algebraic Methods in Programming
Amir Jahangard-Rafsanjani & Seyed-Hassan Mirian-Hosseinabadi - 2015 - Elsevier

Model-driven development meets security: An evaluation of current approaches

System Sciences (HICSS), 2011 44th Hawaii International Conference on
Kresimir Kasal & Johannes Heurix & Thomas Neubauer - 2011

Translating vdm to alloy

Integrated Formal Methods
Kenneth Lausdahl - 2013

Solving Clafer Models with Choco

Jimmy Liang - 2012 - GSDLab-TR

Implementing QVT-R bidirectional model transformations using Alloy

Fundamental Approaches to Software Engineering
Nuno Macedo & Alcino Cunha - 2013 - Springer

A manifesto for semantic model differencing

Models in Software Engineering
Shahar Maoz & Jan Oliver Ringert & Bernhard Rumpe - 2011 - Springer

Solving Design Tasks in Engineering Using Object-Oriented Graph-Based Representations and Boolean Satisfiability

ASME 2013 International Design Engineering Technical Conferences and Computers and Information in Engineering Conference
Clemens Munzer & Kristina Shea & Bergen Helms - 2013

Challenges in Integrating the Analysis of Multiple Non-Functional Properties in Model-Driven Software Engineering

Proceedings of the 2015 Workshop on Challenges in Performance Methods for Software Development
Dorina C Petriu - 2015

Transform both sides model: A parametric approach

Computational Statistics & Data Analysis
A Polpo & CP De Campos & D Sinha et al. - 2014 - Elsevier

Towards Testing Model Transformation Chains Using Precondition Construction in Algebraic Graph Transformation

AMT 2014--Analysis of Model Transformations Workshop Proceedings
Elie Richa & Etienne Borde & Laurent Pautet et al. - 2014

Supporting Iterative Development of Robust Operation Contracts in UML Requirements Models

High-Assurance Systems Engineering (HASE), 2011 IEEE 13th International Symposium on
Wuliang Sun & Robert B France & Indrakshi Ray - 2011

Systematic diagram refinement for code generation in SEAM

Knowledge and Systems Engineering (KSE), 2012 Fourth International Conference on
Quan Thanh Tho & others - 2012

Model transformation analysis: Staying ahead of the maintenance nightmare

Theory and Practice of Model Transformations
Marcel F Van Amstel & Mark GJ Van Den Brand - 2011 - Springer

Assessing the Kodkod model finder for resolving model inconsistencies

Modelling Foundations and Applications
Ragnhild Van Der Straeten & Jorge Pinna Puissant & Tom Mens - 2011 - Springer

Systematic scenario-based analysis of UML design class models

Engineering of Complex Computer Systems (ICECCS), 2012 17th International Conference on
Lijun Yu & Robert B France & Indrakshi Ray et al. - 2012

Developing Model-Driven Software Product Lines

Xiaorui Zhang - 2014

A manifesto for semantic model differencing

S Maoz, J Ringert... - Models in Software Engineering, 2011 - Springer

A lightweight approach for defining the formal semantics of a modeling language

P Kelsen... - Model Driven Engineering Languages and Systems, 2008 - Springer

Assessing the Kodkod model finder for resolving model inconsistencies

R Van Der Straeten, J Pinna Puissant... - Modelling Foundations and ..., 2011 - Springer

Network Protocols

Modeling and analysis of RFID authentication protocols for supply chain management

Parallel, Distributed and Grid Computing (PDGC), 2014 International Conference on
Adarsh Kumar & Krishna Gopal & Alok Aggarwal - 2014

Simulation and analysis of authentication protocols for mobile Internet of Things (MIoT)

Parallel, Distributed and Grid Computing (PDGC), 2014 International Conference on
Adarsh Kumar & Krishna Gopal & Alok Aggarwal - 2014

Detecting Network Policy Conflicts Using Alloy

Abstract State Machines, Alloy, B, TLA, VDM, and Z
Ferney A Maldonado-Lopez & Jaime Chavarriaga & Yezid Donoso - 2014 - Springer

Using Alloy to Formally Model and Reason About an OpenFlow Network Switch

Computer Science Department, Boston University, Tech.
Saber Mirzaei & Sanaz Bahargam & Richard Skowyra et al. - 2013

Formal verification of oauth 2.0 using alloy framework

Communication Systems and Network Technologies (CSNT),
2011 International Conference on
Suhas Pai & Yash Sharma & Sunil Kumar et al. - 2011

A (not) nice way to verify the OpenFlow switch specification: formal modelling of the OpenFlow switch using alloy

ACM SIGCOMM Computer Communication Review
Natali Ruchansky & Davide Proserpio - 2013

Formal analysis of pure-join model of chord using alloy

Software Engineering and Service Science (ICSESS), 2013 4th IEEE International Conference on
Hooman Sadeghian & Alborz Samadi & Hassan Haghighi - 2013

Corrigendum to:“Multi-scale dendritic needle network model of alloy solidification”[Acta Mater. 61 (2013)

Acta Materialia
D Tourret & A Karma - 2015

A formal approach to the design and implementation of configuration strategy automation for switch network

Journal of Tsinghua University Science and Technology
Jiahai Yang & Ning Jiang & Changqing An et al. - 2012 - Tsinghua University Press, Tsinghua University Beijing 100084 China

How to Make Chord Correct (Using a Stable Base)

arXiv preprint arXiv:1502.06461
Pamela Zave - 2015

Compositional Models of Network Architecture

Pamela Zave - 2014

Using lightweight modeling to understand chord

ACM SIGCOMM Computer Communication Review
Pamela Zave - 2012 - ACM

Compositional network mobility

Verified Software: Theories, Tools, Experiments
Pamela Zave & Jennifer Rexford - 2014 - Springer

Toward a lightweight model of BGP safety

M Arye, R Harrison, R Wang, P Zave, J Rexford - Int Workshop on Rigorous Protocol Engineering 2011

Counterexamples to correctness of the Chord ring-maintenance protocol

P Zave - 2010 -

Why the Chord ring-maintenance protocol is not correct

P Zave - 2011 -

Lightweight Modeling of Network Protocols in Alloy

P Zave - 2009 -

Compositional binding in network domains

P Zave - International Symposium on Formal Methods, 2006 -

A formal model of addressing for interoperating networks

P Zave - International Symposium of Formal Methods Europe, 2005

Testing and Automated Test Case Generation

Improving test generation under rich contracts by tight bounds and incremental SAT solving

Software Testing, Verification and Validation (ICST), 2013 IEEE Sixth International Conference on
Pablo Abad & Nazareno Aguirre & Valeria Bengolea et al. - 2013

BloomUnit: Declarative testing for distributed programs

Proceedings of the Fifth International Workshop on Testing Database Systems
Peter Alvaro & Andrew Hutchinson & Neil Conway et al. - 2012

Specification-driven unit test generation for java generic classes

Integrated Formal Methods
Francisco Rebello de Andrade & Joao P Faria & Antónia Lopes et al. - 2012

Test Generation from Bounded Algebraic Specifications using Alloy.

Francisco Rebello de Andrade & João Pascoal Faria & Ana CR Paiva - 2011

ACM SIGSOFT Impact Paper Award 2012: Systematic Software Testing: The Korat Approach

Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering
Chandrasekhar Boyapati & Sarfraz Khurshid & Darko Marinov - 2012

CEGPairGen: An Automated Tool for Generating Pairwise Tests from Cause-Effect Graphs

International Journal of Software Engineering and Its Applications
Insang Chung - 2015

Model-based conformance testing for android

Advances in Information and Computer Security
Yiming Jing & Gail-Joon Ahn & Hongxin Hu - 2012 - Springer

JTACO: Test Execution for Faster Bounded Verification

Tests and Proofs
Alexander Kampmann & Juan Pablo Galeotti & Andreas Zeller - 2014 - Springer

Generating semantically valid test inputs using constrained input grammars

Information and Software Technology
Hossein Keramati & Seyed-Hassan Mirian-Hosseinabadi - 2015 - Elsevier

Mixed constraints for test input generation-An initial exploration

Proceedings of the 2011 26th IEEE/ACM International Conference on Automated Software Engineering
Shadi Abdul Khalek & Vidya Priyadarshini Narayanan & Sarfraz Khurshid - 2011

TestEra: A tool for testing Java programs using alloy specifications

Proceedings of the 2011 26th IEEE/ACM international conference on automated software engineering
Shadi Abdul Khalek & Guowei Yang & Lingming Zhang et al. - 2011

A Symbolic Execution Algorithm for Constraint-Based Testing of Database Programs

arXiv preprint arXiv:1501.05821
Michaël Marcozzi & Wim Vanhoof & Jean-Luc Hainaut - 2015

A relational symbolic execution algorithm for constraint-based testing of database programs

Source Code Analysis and Manipulation (SCAM), 2013 IEEE 13th International Working Conference on
Michaël Marcozzi & Wim Vanhoof & J-L Hainaut - 2013

Test input generation for database programs using relational constraints

Proceedings of the Fifth International Workshop on Testing Database Systems
Michaël Marcozzi & Wim Vanhoof & Jean-Luc Hainaut - 2012

A 5-step hunt for faults in Java implementations of algebraic specifications

Software Testing, Verification and Validation Workshops (ICSTW), 2013 IEEE Sixth International Conference on
Isabel Nunes & Filipe Luıs - 2013

TacoFlow: optimizing sat program verification using dataflow analysis

Software & Systems Modeling
Bruno Cuervo Parrino & Juan Pablo Galeotti & Diego Garbervetsky et al. - 2014 - Springer

EQ: Checking the implementation of equality in Java

Software Maintenance (ICSM), 2011 27th IEEE International Conference on
Chandan Raj Rupakheti & Daqing Hou - 2011

Testing a Data-Intensive System with Generated Data Interactions

Advanced Information Systems Engineering
Sagar Sen & Arnaud Gotlieb - 2013

AUnit-a testing framework for alloy

Allison Sullivan - 2014

Towards a test automation framework for alloy

Proceedings of the 2014 International SPIN Symposium on Model Checking of Software
Allison Sullivan & Razieh Nokhbeh Zaeem & Sarfraz Khurshid et al. - 2014

PARADIGM-COV: A multimensional test coverage analysis tool

Information Systems and Technologies (CISTI), 2014 9th Iberian Conference on
Liliana Vilela & Ana CR Paiva - 2014

Specification-based test repair using a lightweight formal method

FM 2012: Formal Methods
Guowei Yang & Sarfraz Khurshid & Miryung Kim - 2012 - Springer

Automation of Model-Based Testing through Model Transformations

EG Aydal... - Testing: Academic and Industrial ..., 2009 -

Automated SQL query generation for systematic testing of database engines

S Abdul Khalek... - ... of the IEEE/ACM international conference ..., 2010 -

Evaluation of Automated Design Testing using Alloy

J Andersson... - Software Engineering Research ..., 2007 -

Putting formal specifications under the magnifying glass: Model-based testing for validation

EG Aydal, RF Paige, M Utting... - ... Testing Verification and ..., 2009 -

Pairwise testing for software product lines: comparison of two approaches

G Perrouin, S Oster, S Sen, J Klein, B Baudry... - Software Quality ..., 2011 - Springer

Pairwise testing of dynamic composite services

A Kattepur, S Sen, B Baudry, A Benveniste... - Proceeding of the 6th ..., 2011 -

Systematic Testing of Database Engines Using a Relational Constraint Solver

SA Khalek... - Software Testing, Verification and ..., 2011 -

Test data generation for web application using a UML class diagram with OCL constraints

S Fujiwara, K Munakata, Y Maeda... - Innovations in Systems ..., 2011 - Springer

Relational Constraint Driven Test Case Synthesis for Web Applications

X Fu - Arxiv preprint arXiv:1009.3713, 2010 -

Pairwise testing for software product lines: comparison of two approaches

G Perrouin, S Oster, S Sen, J Klein, B Baudry... - Software Quality ..., 2011 - Springer

Configuration and Reconfiguration, Data Structure Repair

Indirect dependencies in dynamic reconfiguration of component-based systems

Software Engineering and Service Science (ICSESS), 2014 5th IEEE International Conference on
Mohammad Charaf Eddin & Zoubir Mammeri - 2014

Synthesis of Configuration Change Procedure Using Model Finder

IEICE TRANSACTIONS on Information and Systems
Shinji Kikuchi & Satoshi Tsuchiya & Kunihiko Hiraishi - 2013 - The Institute of Electronics, Information and Communication Engineers

On the simplicity of synthesizing linked data structure operations

Darya Kurilova & Derek Rayside - 2013

Data model property inference and repair

Proceedings of the 2013 International Symposium on Software Testing and Analysis
Jaideep Nijjar & Tevfik Bultan - 2013

FORS: Separating Configuration From Formal Specification

C Peters - 2014

History-aware data structure repair using SAT

Tools and Algorithms for the Construction and Analysis of Systems
Razieh Nokhbeh Zaeem & Divya Gopinath & Sarfraz Khurshid et al. - 2012 - Springer

Reliable dynamic reconfigurations in a reflective component model

M Leger, T Ledoux... - Component-Based Software ..., 2010 - Springer

Configuration procedure synthesis for complex systems using model finder

S Kikuchi... - Engineering of Complex Computer ..., 2010 -

Security Domain Model and Implementation Modeling

M Auguston, A Shaffer - 2008 -

Contract-Based Data Structure Repair Using Alloy

R Nokhbeh Zaeem... - ECOOP 2010-Object-Oriented ..., 2010 - Springer

Supporting change propagation in the evolution of enterprise architectures

HK Dam, LS Le... - Enterprise Distributed Object ..., 2010 -

Formal Logic Based Configuration Modeling and Verification for Dynamic Component Systems

Z Theisz, G Batori... - MOPAS 2011, The Second ..., 2011 -

A formal approach to software synthesis for architectural platforms

H Bagheri - ... (ICSE), 2011 33rd International Conference on, 2011 -

Network configuration management via model finding

S Narain - Proceedings of the 19th conference on Large ..., 2005 -


Model to specify real time system using Z and alloy languages: A comparative approach

Ashish Kumar Dwivedi & Santanu Ku Rath - 2012 - IET

Requirement progression: deriving specifications through problem diagrams

Joeri Peters - 2014

Generating Alloy Specification: From Textual User Requirements Written in Natural Language

Kiramat Rahman & Shabaz Ahmed Khan Ghayure - 2012 - LAP Lambert Academic Publishing

Requirements modeling in SEAM: The example of a car crash management system

Comparing Requirements Modeling Approaches Workshop (CMA@ RE), 2013 International
Alain Wegmann & Biljana Bajic-Bizumic & Arash Golnam et al. - 2013

Safety process improvement with POSE and Alloy

D Mannering, JG Hall... - Improvements in System Safety, 2008 - Springer