TY - GEN
T1 - Optimizing network deployment of formally-specified distributed systems
AU - Coffrin, Carleton
AU - Michel, Laurent D.
AU - Shvartsman, Alexander A.
AU - Sonderegger, Elaine L.
AU - Van Hentenryck, Pascal
N1 - DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.
PY - 2009
Y1 - 2009
N2 - Formal specifications are indispensable in the design of verifiable complex distributed systems, and formal methods have received considerable attention in that respect. However, the full potential of formal methods can only be realized if the transition from specification to actual implementation can be automated to preserve the properties that were established and proved in the specification. Tempo is an integrated development environment that implements the Timed Input/Output Automata (TIOA) language and can be used to model and verify distributed, concurrent, and timed systems as collections of interacting state machines. In Tempo, individual software modules are modeled as separate automata, while complex distributed systems are modeled through composition mechanisms. To build and deploy an actual distributed system, one must both derive an implementation that is consistent with the formal specification and solve an optimization problem (often NP-hard) to match the software components with the computing resources within the target network, given criteria such as minimizing the resulting network load. This paper assumes that an implementation is available and focuses on the second problem. Namely, it presents new Tempo features for specifying deployment requirements and automatically solving the resulting optimization problem with constraint programming techniques. The new annotation features describe the target platform as well as satisfiability constraints (e.g., physical separation of the software modules implementing replicas in a distributed data service). The augmented specification is translated into a COMET program to compute the optimal deployment. The current set of annotations handles the minimization of communication cost. The implementation can solve hard instances that are beyond the capabilities of modern mixed-integer programming solvers. The paper illustrates this process using a distributed eventually-serializable data service.
AB - Formal specifications are indispensable in the design of verifiable complex distributed systems, and formal methods have received considerable attention in that respect. However, the full potential of formal methods can only be realized if the transition from specification to actual implementation can be automated to preserve the properties that were established and proved in the specification. Tempo is an integrated development environment that implements the Timed Input/Output Automata (TIOA) language and can be used to model and verify distributed, concurrent, and timed systems as collections of interacting state machines. In Tempo, individual software modules are modeled as separate automata, while complex distributed systems are modeled through composition mechanisms. To build and deploy an actual distributed system, one must both derive an implementation that is consistent with the formal specification and solve an optimization problem (often NP-hard) to match the software components with the computing resources within the target network, given criteria such as minimizing the resulting network load. This paper assumes that an implementation is available and focuses on the second problem. Namely, it presents new Tempo features for specifying deployment requirements and automatically solving the resulting optimization problem with constraint programming techniques. The new annotation features describe the target platform as well as satisfiability constraints (e.g., physical separation of the software modules implementing replicas in a distributed data service). The augmented specification is translated into a COMET program to compute the optimal deployment. The current set of annotations handles the minimization of communication cost. The implementation can solve hard instances that are beyond the capabilities of modern mixed-integer programming solvers. The paper illustrates this process using a distributed eventually-serializable data service.
KW - Constraint programming
KW - Distributed systems
KW - Formal specification
KW - Input/output automata
KW - Optimal deployment
UR - http://www.scopus.com/inward/record.url?scp=84883311639&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84883311639&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:84883311639
SN - 9781615672417
T3 - 18th International Conference on Software Engineering and Data Engineering 2009, SEDE 2009
SP - 230
EP - 237
BT - 18th International Conference on Software Engineering and Data Engineering 2009, SEDE 2009
T2 - 18th International Conference on Software Engineering and Data Engineering 2009, SEDE 2009
Y2 - 22 June 2009 through 24 June 2009
ER -