A proof system for MDESL

• Autorzy: Lu Jianyu , Xie Wanling , Zhu Huibiao , Fei Yuan

Identyfikatory

DOI

10.15439/2017F400

• Konferencja: Communication Papers of the 2017 Federated Conference on Computer Science and Information Systems
• Języki publikacji: EN

Abstrakty

EN

Hardware description language (HDL) Verilog has been standardized and widely used in industry. To describe the features such as event-driven computation, time and shared-variable concurrency of hardware, a Verilog-like language MDESL (multithreaded discrete event simulation language), has been introduced. In this paper, we put forward a proof system for MDESL which is based on the classical Hoare Logic (precondition, program, postcondition). To deal with the guard statement, we add a new element trace to Hoare triples. We extend the primitives of assertion to express the global time of current program, and interpret the triples so that it can verify both terminating and nonterminating computations. To verify a concurrent program, we use a merger method of the trace to combine the traces in our parallel rule. Finally, there is an example about using our proof system to verify the correctness of a program written by MDESL.

• Wydawca: Polskie Towarzystwo Informatyczne
• Czasopismo: Annals of Computer Science and Information Systems
• Rocznik: 2017
• Tom: Vol. 13
• Strony: 387--393
• Opis fizyczny: Bibliogr. 15 poz., rys.

Twórcy

autor

Lu Jianyu

• Shanghai Key Laboratory of Trustworthy Computing, School of Computer and Software Engineering, East China Normal University, Shanghai, China

autor

Xie Wanling

• Shanghai Key Laboratory of Trustworthy Computing, School of Computer and Software Engineering, East China Normal University, Shanghai, China

autor

Zhu Huibiao

• Shanghai Key Laboratory of Trustworthy Computing, School of Computer and Software Engineering, East China Normal University, Shanghai, China

autor

Fei Yuan

• Shanghai Key Laboratory of Trustworthy Computing, School of Computer and Software Engineering, East China Normal University, Shanghai, China

Bibliografia

• 1. IEEE, IEEE Standard Hardware Description Language based on the Verilog Hardware Description Laguage, Volume IEEE Standard 1364-1995. IEEE, 1995.
• 2. IEEE, IEEE Standard Hardware Description Language based on the Verilog Hardware Description Laguage, Volume IEEE Standard 1364-2001. IEEE, 2001.
• 3. N. Nissanke, Realtime Systems, Prentice Hall International Series in computer Science, 1997.
• 4. Haase, V., Real-time Behavior of Programs, IEEE Transactions on Software Engineering SE-7,5 (Sept. 1981), 497-501.
• 5. Zhu, H., Linking the Semantics of a Multithreaded Discrete Event Simulation Language, London South Bank University, 2005.
• 6. Golze, U., VLSI Chip Design with the Hardware Description Language Verilog: An Introduction Based on a Large RISC Processor Design, Springer-Verlag New York, Inc. 1996.
• 7. Gordon, M.J.C., The semantic challenge of Verilog HDL, In Proc. Tenth Annual IEEE Symposium on Logic in Computer Science, page 136-145. IEEE Computer Society Press, June 1995.
• 8. Gordon, M.J.C., Relating event and trace semantics of hardware description languages, The Computer Journal, 45(1): 27-36, 2002.
• 9. Apt, K.R., de Boer, F.S., Olderog, E., Verification of sequential and concurrent programs, Texts in Computer Science, Springer, 2009.
• 10. Hoare, C.A.R., Communicating Sequential Processes, Prentice Hall International Series in Computer Science, 1985.
• 11. Hooman, J., Extending hoare logic to real-time, Formal Aspects of Computing, 1994, 6(1):801-825.
• 12. Park, S., Pfenning, F., Thrun, S., A probabilistic language based upon sampling functions, Acm Transactions on Programming Languages, 2004, 40.1(2004):171-182.
• 13. Zhu, H., Qin, S., He, J., Bowen, J.P., PTSC: probaility, time and shared-variable concurrency, Innovations in Systems and Software Enginerring: A NASA Journal 5(4), 271-284(2009).
• 14. Hoare, C. A. R., Algebra of concurrent programming, In: Meeting 52 of WG 2.3(2011).
• 15. Hoare, C. A. R., He, J., Unifying Theories of programming, Prentice Hall International Series in Computer Science, 1998.