In recent years, the language PSL (Property Specification Language, a.k.a. IEEE P1850) has been embraced and put to successful use by chip design/verification engineers across the electronics industry. While PSL is mainly used for hardware verification, it can, in fact, be used to verify a wide variety of systems, including missile interception systems, railway interlocking protocols, system automation policies, and even business processes.We discuss and exemplify how PSL can be used as a general purpose language for the specification of models and properties, beyond hardware 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
Dakshi Agrawal et al. Policy Management of Networked Systems and Applications. In Proc. of 9th Intl. Symp. on Integrated Network Management, IFIP/IEEE 2005.
S. Barner, Z. Glazberg, and I. Rabinovitz. Wolf—Bug Hunter for Concurrent Software Using Formal Methods. In Proc. of 17th International Conference on Computer Aided Verification, LNCS 3576, Springer, 2005.
S. Barner and I. Rabinovitz. Efficient symbolic model checking of software using partial dis-junctive partitioning. CHARME, LNCS 2860, 2003.
I. Beer et al. RuleBase: An Industry-Oriented Formal Verification Tool. In Proc. of the 33rd Design Automation Conference, 1996.
G. Booch, J. E. Rumbaugh, and I. Jacobson. Unified Modeling Language User Guide. Addison- Wesley, 1999.
D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the Association for Computing Machinery, 30(2), 1983.
Cindy Eisner, Dana Fisman. A Practical Introduction to PSL. Springer, August 2005.
Janees Elamkulam et al. Detecting Design Flaws in UML State Charts for Embedded Software, to In Proc. of Haifa Verification Conference HVC 2006. LNCS 4383, Springer, 2006.
E.M. Clarke and E.A. Emerson, Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. In Proc. of Workshop on Logics of Programs, LNCS 131, Springer, 1981.
D. Ghose. True Proportional Navigation with Maneuvering Target, IEEE Trans. on Aerospace and Electronic Systems, 1994.
C.-F. Lin. Modern Navigation, Guidance and Control Processing. Prentice Hall, 1991.
M. Moulin, L. Gluhovsky, and E. Bendersky. Formal Verification of Maneuvering Target Track- ing. Proc. of the AIAA Conf. of Guidance, Navigation and Control, Austin, TX, 2003.
A. Pnueli. A Temporal Logic of Concurrent Programs. In Theoretical Computer Science, Vol 13,1981.
M. L. Steinberg. Comparison of Intelligent, Adaptive, and Nonlinear Flight Control Laws, Jour- nal of Guidance, Control and Dynamics, 2001.
A. van der Schaft, H. Schumacher. An Introduction to Hybrid Dynamical Systems. Springer, 2000. V.251 of Lecture Notes in Control and Information Sciences.
A. Wasowski. Flattening Statecharts without Explosions. In Proc. of the 2004 ACM SIG-PLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, 2004.
S. Wright, R. Chadha, and G. Lapiotis (eds): Special Issue on Policy Based Networking, IEEE Networking 16, 2002.
Emmanuel Zarpas. A Case Study: Formal Verification of Processor Critical Properties, Correct Hardware Design and Verification Methods: CHARME 2005, LNCS 3725, Springer 2005.
IBM Tivoli System Automation for Multi-platforms, Guide and Reference, version 1.2, IBM, 2004.
IBM Tivoli System Automation for Multi-platforms, Base Component Reference, version 2.1.1, 2006.
IEEE Standard for Property Specification Language IEEE Std. 1850-2005, 2005.
RuleBase PE homepage. http://www.haifa.il.ibm.com/projects/verification/RB Homepage/index.html, 2006
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2007 Springer
About this paper
Cite this paper
Glazberg, Z., Moulin, M., Orni, A., Ruah, S., Zarpas, E. (2007). PSL: Beyond Hardware Verification. In: Ramesh, S., Sampath, P. (eds) Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems. Springer, Dordrecht. https://doi.org/10.1007/978-1-4020-6254-4_19
Download citation
DOI: https://doi.org/10.1007/978-1-4020-6254-4_19
Publisher Name: Springer, Dordrecht
Print ISBN: 978-1-4020-6253-7
Online ISBN: 978-1-4020-6254-4
eBook Packages: EngineeringEngineering (R0)