Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Kết hợp các Kỹ thuật Kiểm tra Phần mềm và Phần cứng
Tóm tắt
Việc kết hợp các phương pháp xác thực được phát triển tách biệt cho phần mềm và phần cứng được thúc đẩy bởi nhu cầu của ngành công nghiệp về một công nghệ sẽ làm cho việc xác thực chính xác các thiết kế kết hợp phần mềm/phần cứng thực tiễn trở nên khả thi. Chúng tôi tập trung vào những kỹ thuật đã chứng minh thành công trong mỗi lĩnh vực: kiểm tra mô hình biểu diễn dạng đồ thị nhị phân (BDD) cho việc xác thực phần cứng và giảm bậc một phần cho việc xác thực các chương trình phần mềm đồng thời. Trong bài báo này, chúng tôi trước tiên đề xuất một sự điều chỉnh của giảm bậc một phần, cho phép kết hợp nó với bất kỳ công cụ xác thực dựa trên BDD nào, và sau đó mô tả một phương pháp xác thực chung được phát triển bằng cách sử dụng các kỹ thuật này phối hợp. Kết quả thí nghiệm của chúng tôi chứng minh hiệu quả của kỹ thuật xác thực kết hợp này, và gợi ý rằng đối với các hệ thống có kích thước vừa phải, phương pháp này đã sẵn sàng để ứng dụng trong công nghiệp.
Từ khóa
#Xác thực phần mềm #xác thực phần cứng #kiểm tra mô hình dựa trên BDD #giảm bậc một phần #thiết kế kết hợp phần mềm/phần cứngTài liệu tham khảo
R. Alur, R.K. Brayton, T.A. Henzinger, S. Qadeer, and S.K. Rajamani, “Partial-order reduction in symbolic state space exploration,” in O. Grumberg (ed.), Computer Aided Verification, 9th International Conference, (CAV '97) Proceedings, Vol. 1254 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1997, pp. 340-351.
B. Berger and P.W. Shor, “Approximation algorithms for the maximum acyclic subgraph problem,” in First ACM-SIAM Symp. on Discrete Algorithms. Proceedings, 1990, pp. 236-243.
C.-T. Chou and D. Peled, “Formal verification of a partial-order reduction technique for model checking,” in T. Margaria and B. Steffen (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Second InternationalWorkshop (TACAS '96) Proceedings, Vol. 1055 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1996, pp. 241-257.
D.L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, Cambridge, MA, 1989.
D. Dolev, M. Klawe, and M. Rodeh, “An O(n log n) unidirectional distributed algorithm for extrema finding in a circle,” Journal of Algorithms, Vol. 3, No. 3, pp. 245-260, 1982.
P. Eades, X. Lin, and W.M. Smyth, “Afast and effective heuristic for the feedback arc set problem,” Information Processing Letters, Vol. 47, No. 6, pp. 319-323, 1993.
D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, “On the temporal analysis of fairness,” in Conference Record of the Seventh ACM Symposium on Principles of Programming Languages, 1980, pp. 163-173.
P. Godefroid and D. Pirottin, “Refining dependencies improves partial-order verification methods,” in C. Courcoubetis (Ed.), Computer Aided Verification, 5th International Conference (CAV '93) Proceedings, Vol. 697 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1993, pp. 438-449.
R.H. Hardin, Z. Har'El, and R.P. Kurshan, “COSPAN,” in R. Alur and T.A. Henzinger (Eds.), Computer Aided Verification, 8th International Conference (CAV '96) Proceedings, Vol. 1102 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1996, pp. 423-427.
Z. Har'El and R.P. Kurshan, “Software for analytical development of communication protocols,” AT&T Technical Journal, Vol. 69, No. 1, pp. 45-59, 1990.
G.J. Holzmann, “The model checker Spin,” IEEE Trans. on Software Engineering,Vol. 23, No. 5, pp. 279-295, 1997.
G.J. Holzmann and D. Peled, “An improvement in formal verification,” in D. Hogrefe and S. Leue (Eds.), Formal Description Techniques VII, Proceedings of the 7th IFIP WG 6.1 International Conference Bern, Switzerland, 1994, pp. 197-211.
R.M. Karp, “Reducibility among combinatorial problems,” in Complexity of Computer Computations, Plenum Press, New York, 1972, pp. 85-103.
R.P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach, Princeton University Press, Princeton, NJ, 1994.
R. Kurshan, V. Levin, M. Minea, D. Peled, and H. Yenigün, “Static partial order reduction,” in B. Steffen (Ed.), Tools and Algorithms for the Construction and Analysis of Systems, 4th International Conference (TACAS'98) Proceedings, Vol. 1384 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1998, pp. 345-357.
R.P. Kurshan, M. Merritt, A. Orda, and S. Sachs, “Modeling asynchrony with a synchronous model,” in P. Wolper (Ed.), Computer Aided Verification, 7th International Conference (CAV'95) Proceedings, Vol. 939 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995, pp. 339-352.
L. Lamport, “What good is temporal logic,” in R.E.A. Mason (Ed.), Proceedings of IFIP Congress, North Holland, 1983, pp. 657-668.
V. Levin, E. Bounimova, O. Başbuğoğlu, and K. İnan, “A verifiable software/hardware co-design using SDL and COSPAN,” in Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design, Maribor, Slovenia, 1996, pp. 6-16.
V. Levin and H. Yenigün, “SDLCheck: A model checking tool,” in G. Berry, H. Comon, and A. Finkel (Eds.), Computer Aided Verification, 13th International Conference (CAV 2001) Proceedings, Vol. 2102 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 2001, pp. 378-381.
K.L. McMillan, Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1993.
D. Peled, “Combining partial order reductions with on-the-fly model-checking,” Formal Methods in System Design, Vol. 8, pp. 39-64, 1996.
D. Peled and T. Wilke, “Stutter-invariant temporal properties are expressible without the next-time operator,” Information Processing Letters, Vol. 63, No. 5, pp. 243-246, 1997.
SDL92, “Functional specification and description language (SDL), ITU-T Recommendation Z.100,” 1993, Geneva.
N. Sharygina, R.P. Kurshan, and J.C. Browne, “A formal object-oriented analysis for software reliability: Design for verification,” in Heinrich Husmann (Ed.), Fundamental Approaches to Software Engineering, 4th International Conference (FASE 2001) Proceedings, Vol. 2029 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 2001, pp. 318-332.
S. Shlaer and S.J. Mellor, Object Lifecycles Modeling the World in States, Prentice-Hall, Englewood Cliffs, NJ, 1992.
A. Valmari, “A stubborn attack on state explosion,” in E.M. Clarke and R.P. Kurshan (Eds.), Computer-Aided Verification, 2nd International Conference (CAV '90) Proceedings, Vol. 531 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1990, pp. 156-165.
Verilog95, “IEEE standard hardware description language based on the VerilogTM hardware description language, “IEEE Std 1364-1995,” 1996, New York.
VHDL93, “IEEE Standard VHDL Language Reference Manual, IEEE Std 1076-1993,” 1994, New York.