PSL: Beyond Hardware Verification
作者： Ziv Glazberg , Mark Moulin , Avigail Orni , Sitvanit Ruah , Emmanuel Zarpas
DOI: 10.1007/978-1-4020-6254-4_19
关键词: Integrated circuit design 、 Computer hardware 、 Business process 、 Automation 、 Variety (cybernetics) 、 Finite-state machine 、 General-purpose language 、 Property Specification Language 、 Engineering 、 Electronics
摘要: 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 electronics industry. While is mainly used for hardware ver- ification, it can, in fact, be verify a wide variety of systems, including missile interception railway interlocking protocols, system automation policies, even business processes. We discuss exemplify how can as general purpose specification models properties, beyond systems.
springer.com
researchgate.net 
sci-hub.st 参考文章(18)
Cindy Eisner, Dana Fisman, A Practical Introduction to PSL (Series on Integrated Circuits and Systems) Springer-Verlag New York, Inc.. ,(2006)
Ching-Fang Lin, Modern Navigation, Guidance, And Control Processing ,(1991)
Edmund M. Clarke, E. Allen Emerson, DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC 25 Years of Model Checking. ,vol. 131, pp. 196- 215 ,(2008) , 10.1007/978-3-540-69850-0_12
Sharon Barner, Ishai Rabinovitz, Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning Lecture Notes in Computer Science. pp. 35- 50 ,(2003) , 10.1007/978-3-540-39724-3_6
Janees Elamkulam, Ziv Glazberg, Ishai Rabinovitz, Gururaja Kowlali, Satish Chandra Gupta, Sandeep Kohli, Sai Dattathrani, Claudio Paniagua Macia, Detecting Design Flaws in UML State Charts for Embedded Software Lecture Notes in Computer Science. ,vol. 4383, pp. 109- 121 ,(2007) , 10.1007/978-3-540-70889-6_8
Emmanuel Zarpas, A Case Study: Formal Verification of Processor Critical Properties Lecture Notes in Computer Science. pp. 406- 409 ,(2005) , 10.1007/11560548_42
Sharon Barner, Ziv Glazberg, Ishai Rabinovitz, Wolf – Bug Hunter for Concurrent Software Using Formal Methods Computer Aided Verification. pp. 153- 157 ,(2005) , 10.1007/11513988_16
J. M. Schumacher, Schaft A. J. van der, An Introduction to Hybrid Dynamical Systems ,(1999)
Amir Pnueli, The temporal semantics of concurrent programs Theoretical Computer Science. ,vol. 13, pp. 45- 60 ,(1981) , 10.1016/0304-3975(81)90110-9
Daniel Brand, Pitro Zafiropulo, On Communicating Finite-State Machines Journal of the ACM. ,vol. 30, pp. 323- 342 ,(1983) , 10.1145/322374.322380