Abstract
This paper presents the results of an industrial case-study concerning the use of formal methods for the validation of hardware design. The case-study focuses on PowerScaleTM, a multiprocessor architecture based on PowerPCTM micro-processors and used in Bull’s EscalaTM series of servers and workstations*. The specification language Lotos (ISO International Standard 8807) was used to describe formally the main components of this architecture (processors, memory controller and bus arbiter). Four correctness properties were identified, which express the essential requirements for a proper functioning of the arbitration algorithm, and formalized in terms of bisimulation relations (modulo abstractions) between finite labelled transition systems. Using the compositional and on-the-fly model-checking techniques implemented in the Cadp (CÆsar/Aldêbaran) toolbox, the correctness of the arbitration algorithm was established automatically in a few minutes.
PowerScale and Escala are registered trademarks of Bull. PowerPC is a registered trademark of the International Business Machines Corporation.
Chapter PDF
References
Ahmed Bouajjani, Jean-Claude Fernandez, Susanne Graf, Carlos Rodriguez, and Joseph Sifakis. Safety for Branching Time Semantics. In Proceedings of 18th ICALP, Berlin, July 1991. Springer Verlag.
P. Bennett and A. Ramolini. The Power Scale Architecture: A Technical Overview. Journal of Technical Information for the Distributed Computing Model, January-February 1995.
Jean-Claude Fernandez. An Implementation of an Efficient Algorithm for Bisimulation Equivalence. Science of Computer Programming, 13(2–3):219–236, May 1990.
Jean-Claude Fernandez, Hubert Garavel, Alain Kerbrat, Radu Mateescu, Laurent Mounier, and Mihaela Sighireanu. CADP (CÆSAR/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox. In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings of the 8th Conference on Computer-Aided Verification (New Brunswick, New Jersey, USA), August 1996.
Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodriguez, and Joseph Sifakis. A Toolbox for the Verification of LOTOS Programs. In Lori A. Clarke, editor, Proceedings of the 14th International Conference on Software Engineering ICSE’14 (Melbourne, Australia), pages 246–259, New-York, May 1992. ACM.
Jean-Claude Fernandez, Alain Kerbrat, and Laurent Mounier. Symbolic Equivalence Checking. In C. Courcoubetis, editor, Proceedings of the 5th Workshop on Computer-Aided Verification (Heraklion, Greece), volume 697 of Lecture Notes in Computer Science, Berlin, June 1993. Springer Verlag.
M. Faci and L. Logrippo. Specifying Hardware in LOTOS. In D. Agnew, L. Claesen, and R. Camposano, editors, Proceedings of the the 11th International Conference on Computer Hardware Description Languages and their Applications (Ottawa, Ontario, Canada), pages 305–312, Amsterdam, April 1993. North-Holland.
Hubert Garavel. Compilation of LOTOS Abstract Data Types. In Son T. Vuong, editor, Proceedings of the 2nd International Conference on Formal Description Techniques FORTE’89 (Vancouver B.C., Canada), pages 147–162, Amsterdam, December 1989. North-Holland.
K. Gharachorloo, D. Lenosky, J. Laudon, P. Gibbons, A. Gupta, and J. Hennessy. Memory Consistency and Event Ordering in Scalable Shared-Memory Multiprocessors. In Proceedings of the 17th Annual International Symposium on Computer Architecture, 1990.
Hubert Garavel and Joseph Sifakis. Compilation and Verification of LOTOS Specifications. In L. Logrippo, R. L. Probert, and H. Ural, editors, Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification (Ottawa, Canada), pages 379–394, Amsterdam, June 1990. IFIP, North-Holland.
Hubert Garavel and Philippe Turlier. C/ESAR.ADT: un compilateur pour les types abstraits algébriques du langage LOTOS. In Rachida Dssouli and Gregor v. Bochmann, editors, Actes du Colloque Francophone pour l’Ingénierie des Protocoles CFIP’93 (Montréal, Canada), 1993.
Jan Friso Groote and Frits Vaandrager. An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence. In M. S. Patterson, editor, Proceedings of the 17th ICALP (Warwick), volume 443 of Lecture Notes in Computer Science, pages 626–638, Berlin, 1990. Springer Verlag.
IEEE. Standard VHDL Language Reference Manual. IEEE Standard 1076–1993, Institution of Electrical and Electronic Engineers, 1993.
IEEE. Verilog HDL Language Reference Manual. IEEE Draft Standard 1364, Institution of Electrical and Electronic Engineers, October 1995.
ISO/IEC. ESTELLE — A Formal Description Technique Based on an Extended State Transition Model. International Standard 9074, International Organization for Standardization Information Processing Systems — Open Systems Interconnection, Genève, September 1988.
ISO/IEC. LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Or-ganization for Standardization — Information Processing Systems — Open Systems Interconnection, Genève, September 1988.
ITU-T. Specification and Description Language (SDL). ITU-T Recommendation Z.100, International Telecommunication Union, Genève, 1992.
Robin Milner. Communication and Concurrency. Prentice-Hall, Englewood Cliffs, NJ, 1989.
Laurent Mounier. Méthodes de vérification de spécifications comportementales: étude et mise en oeuvre. Thèse de Doctorat, Université Joseph Fourier (Grenoble), January 1992.
M. S. Papamarcos and J. H. Patel. A Low-Overhead Coherence Solution for Mul-tiprocessors with Private Cache Memories. In Proceedings of the 11th International Symposium on Computer Architecture, 1984.
Richard O. Sinnott and Kenneth J. Turner. DILL: Specifying Digital Logic in LOTOS. In Richard L. Tenney, Paul D. Amer, and M. Umit Uyar, editors, Proceedings of the 6th International Conference on Formal Description Techniques FORTE’93 (Boston, MA, USA), pages 71–86, Amsterdam, October 1993. North-Holland.
R. J. van Glabbeek and W. P. Weijland. Branching-Time and Abstraction in Bisimulation Semantics (extended abstract). CS R8911, Centrum voor Wiskunde en Informatica, Amsterdam, 1989. Also in proc. IFIP 11th World Computer Congress, San Francisco, 1989.
C. Vissers, G. Scollo, and M. van Sinderen. Architecture and Specification Style in Formal Descriptions of Distributed Systems. In S. Aggarwal and K. Sabnani, editors, Proceedings of the 8th International Workshop on Protocol Specification, Testing and Verification (Atlantic City, NJ, USA), pages 189–204, Amsterdam, 1988. IFIP, North-Holland.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Chehaibar, G., Garavel, H., Mounier, L., Tawbi, N., Zulian, F. (1996). Specification and Verification of the PowerScaleTM Bus Arbitration Protocol: An Industrial Experiment with LOTOS. In: Gotzhein, R., Bredereke, J. (eds) Formal Description Techniques IX. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35079-0_28
Download citation
DOI: https://doi.org/10.1007/978-0-387-35079-0_28
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2883-4
Online ISBN: 978-0-387-35079-0
eBook Packages: Springer Book Archive