Abstract
The use of model checkers to solve discrete optimisation problems is appealing. A model checker can first be used to verify that the model of the problem is correct. Subsequently, the same model can be used to find an optimal solution for the problem. This paper describes how to apply the new Promela primitives of Spin 4. 0 to search effectively for the optimal solution. We show how Branch-and-Bound techniques can be added to the LTL property that is used to find the solution. The LTL property is dynamically changed during the verification. We also show how the syntactical reordering of statements and/or processes in the Promela model can improve the search even further. The techniques are illustrated using two running examples: the Travelling Salesman Problem and a job-shop scheduling problem.
This work is partially supported by the European Community IST-2001-35304 Project AMETIST (Advanced Methods for Timed Systems).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Advanced Methods for Timed Systems (AMETIST) Project. IST-2001-35304. Homepage: http://ametist.cs.utwente.nl/.
G. Behrmann, A. Fehnker, T. Hune, K. Larsen, P. Pettersson, and J. Romijn. Efficient Guiding Towards Cost-Optimality in Uppaal. In T. Margaria and W. Yi, editors, Procs. of the 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), volume 2031 of LNCS, pages 174–188, Genova, Italy, April 2001. Springer.
O. S. Benli. The Branch-and-Bound Approach. In Anil Mital, editor, Industrial Engineering Applications and Practice: Users’ Encyclopedia, 1999. CD-ROM edition, chapter available from http://http://www.csulb.edu/~obenli/.
D. Bošnački, D. Dams, and L. Holenderski. Symmetric Spin. In Havelund et al. [9], pages 1–19.
E. Brinksma and A. Mader. Verification and Optimization of a PLC Control Schedule. In Havelund et al. [9], pages 73–92.
S. Edelkamp, A. L. Lafuente, and S. Leue. Directed Explicit Model Checking with HSF-SPIN. In M. B. Dwyer, editor, Model Checking Software, Procs. of the 8th Int. SPIN Workshop, volume 2057 of LNCS, pages 57–79, Toronto, Canada, May 2001. Springer.
A. Fehnker. Scheduling a Steel Plant with Timed Automata. In Procs. of the 6th Int. Conf. on Real-Time Computing Systems and Applications (RTCSA 1999), pages 280–286. IEEE Computer Society, 1999.
A. Fehnker. Citius Vilius Melius — Guiding and Cost-Optimality in Model Checking of Timed and Hybrid Systems. PhD thesis, University of Nijmegen, The Netherlands, April 2002.
K. Havelund, J. Penix, and W. Visser, editors. SPIN Model Checking and Software Verification, Procs. of the 7th Int. SPIN Workshop (SPIN’2000), volume 1885 of LNCS, Stanford, California, USA, August 2000. Springer.
G. J. Holzman. The SPIN Model Checker — Primer and Reference Manual. Addison-Wesley, Boston, USA, 2003.
G. J. Holzmann. Spin homepage: http://spinroot.com/.
G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs, New Jersey, USA, 1991.
G. J. Holzmann. The Model Checker Spin. IEEE Transactions on Software Engineering, 23(5):279–295, May 1997.
G. J. Holzmann, D. Peled, and M. Yannakakis. On Nested Depth First Search. In J.-C. Gr’egoire, G. J. Holzmann, and D. A. Peled, editors, The SPIN Verification System, Procs. of the 2nd Int. SPIN Workshop (SPIN’96), volume 32 of DIMACS Series, Rutgers University, New Jersey, USA, August 1996. AMS.
K. Larsen, G. Behrmann, E. Brinksma, A. Fehnker, T. Hune, P. Pettersson, and J. Romijn. As Cheap As Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. In G. Berry, H. Comon, and A. Finkel, editors, Procs. of the 13th Int. Conf. on Computer Aided Verification (CAV 2001), volume 2102 of LNCS, pages 493–505, Paris, France, July 2001. Springer.
Princeton University, Mathematics Department. Traveling Salesman Problem — Homepage. http://www.math.princeton.edu/tsp/.
G. Reinelt. The Travelling Salesman — Computational Solutions for TSP Applications, volume 840 of LNCS. Springer, 1994.
T. C. Ruys. Low-Fat Recipes for Spin. In Havelund et al. [9], pages 287–321.
T. C. Ruys. Towards Effective Model Checking. PhD thesis, University of Twente, Enschede, The Netherlands, March 2001. Available from the author’s homepage.
T. C. Ruys and E. Brinksma. Experience with Literate Programming in the Modelling and Validation of Systems. In B. Steffen, editor, Procs. of the 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), number 1384 in LNCS, pages 393–408, Lisbon, Portugal, April 1998.
G. S. Shedler. Regenerative Stochastic Simulation. Academic Press, Boston, 1993.
W. L. Winston. Operations Research — Applications and Algorithms. Duxbury Press, Belmont, California, USA, third edition, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ruys, T.C. (2003). Optimal Scheduling Using Branch and Bound with SPIN 4.0. In: Ball, T., Rajamani, S.K. (eds) Model Checking Software. SPIN 2003. Lecture Notes in Computer Science, vol 2648. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44829-2_1
Download citation
DOI: https://doi.org/10.1007/3-540-44829-2_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40117-9
Online ISBN: 978-3-540-44829-7
eBook Packages: Springer Book Archive