F UTURE W ORK

The way we combine SMV and PNV now is calling SMV by PNV when it’s necessary. It means that the two programs are still individual and they need to read the input file one time respectively. If SMV and PNV could be integrated into one program, the information of the input file can be shared between SMV part and PNV part and we don’t need to waste time on reading the input file twice. Combining the two programs can also make users more convenient use the program.

The marking generator is not friendly enough for users. The generating method now is based on the properties and the user should describe the properties amply about each signal and state. If the marking generator could be made smarter, users could describe a property with only mentioning its states of some signals and the generator would filled with appropriate signals to make the property complete.

References

[1] James L. Peterson, PETRI NET THEORY AND THE MODELING OF SYSTEMS, Prentice-Hall, Inc. 1981

[2] Bruce Wile, john C. Goss, Wolfgang Roesner, COMPREHENSIVE FUNCTIONAL VERIFICATION THE COMPLETE INDUSTRY CYCLE, Elsevier Inc. 2005

[3] Edmund M. Clarke, Bernd-Holger Schlingloff, HANDBOOK OF AUTOMATED RESONING, Elsevier Science Publishers B.V. 2001

[4] Giovanni De Micheli, SYNTHESIS AND OPTIMIZATION OF DIGITAL CIRCUITS, McGraw-Hill, Inc. 1994

[5] Varea M., Al-Hashimi B.M., Cortes L.A., Eles P., Zebo Peng, “Symbolic model checking of dual transition Petri Nets”, Hardware/Software Codesign, CODES, pp.43 – 48, May 2002

[6] Zhenyu Chen, Conghua Zhou, Decheng Ding, “Automatic abstraction refinement for Petri nets verification”, IEEE Int. High-Level Design Validation and Test Workshop, pp.168 – 174, Dec. 2005

[7] Karlsson, D., Eles, P., Zebo Peng, “Formal verification in a component-based reuse methodology”, System Synthesis, 15th International Symposium, pp.156 – 161, 2002

[8] Weng X., Litz L., “Verification of logic control design using SIPN and model checking: methods and case study”, American Control Conference, vol.6,

63

pp.4072 - 4076, June 2000

[9] Cortadella J., “Combining structural and symbolic methods for the verification of concurrent systems”, Application of Concurrency to System Design Int., pp.

2 – 7, March 1998

[10] Rodrigues C.L., Guerrero D.D.S., de Figueiredo J.C.A., “Model checking in object-oriented Petri nets”, IEEE Int. Systems, Man and Cybernetics, Vol 5, pp.4977 - 4982, Oct. 2004

[11] Pastor E., Cortadella J., Roig O., “Symbolic analysis of bounded Petri nets”, IEEE Trans. Computers, Vol 50, No. 5, pp.432 – 448, May 2001

[12] Wang J., Deng Y., Xu G., “Reachability analysis of real-time systems using time Petri nets”, IEEE Trans. Systems, Man and Cybernetics, Part B, Vol. 30, No.

5, pp.725 – 736, Oct. 2000

[13] Tsai J.J.P., Jennhwa Yang S., Yao-Hsiung Chang, “Timing constraint Petri nets and their application to schedulability analysis of real-time system specifications”, IEEE Trans. Software Engineering, Vol 21, No. 1, pp.32 – 49, Jan. 1995

[14] Jiang J., Azzopardi D., Holding D.J., Carpenter G.F., Sagoo J.G., “Real-time synchronisation of multiaxis high-speed machines, from SFC specification to Petri net verification”, IEEE Control Theory and Applications, Vol 143, No.

2, pp.164 – 170, March 1996

[15] Tsung-Hsi Chiang, Lan-Rong Dung, Ming-Feng Yaung, “Modeling and formal verification of dataflow graph in system-level design using Petri net”, IEEE Int.

ISCAS, Vol. 6, pp.5674 - 5677, May 2005

[16] Berthomieu B., Diaz M., “Modeling and verification of time dependent systems using time Petri nets”, IEEE Trans. Software Engineering, Vol. 17, No. 3, pp.259 – 273, March 1991

[17] Castelnuovo A., Ferrarini L., Piroddi L., “An incremental Petri net approach to production sequence modeling”, IEEE Int. Automation Science and Engineering, pp.333 – 338, Aug. 2005

[18] Wang J., Deng Y., Zhou M., “Compositional time Petri nets and reduction rules”, IEEE Trans. Systems, Man and Cybernetics, Part B, Vol. 30, No. 4, pp.562 – 572, Aug. 2000

[19] Zurawski R., “Petri net models, functional abstractions, and reduction techniques:

applications to the design of automated manufacturing systems”, IEEE Trans.

Industrial Electronics, Vol. 52, No. 2, pp.595 – 609, April 2005

[20] Hadjidj R., Boucheneb H., “On-the-fly TCTL model checking for Time Petri Nets using state class graphs”, ACSD Int. Application of Concurrency to System Design, pp.111 – 122, June 2006

[21] Yang S.J.H., Chu W., Lin S., Lee J., “Specifying and verifying temporal behavior of high assurance systems using reachability tree logic”, IEEE Int.

High-Assurance Systems Engineering Symposium, pp.150 – 156, Nov. 1998 [22] Emerson, E.A.; Namjoshi, K.S., “On model checking for non-deterministic

infinite-state systems”, IEEE Sym. Logic in Computer Science, pp.70 – 80, June 1998

[23] NuSMV source code, http://nusmv.irst.itc.it/

[24] SMV source code and execution file, Model Checking Group in Specification and Verification Center at CMU, http://www.cs.cmu.edu/~modelcheck/smv.html [25] Cadence SMV model checker, Cadence Berkeley Labs,

http://www.kenmcmil.com/smv.html

[26] J. R. Burch, E. M. Clarke, D. E. Long, “Symbolic model checking with partitioned transition relations”, In VLSI 91, Edinburgh, Scotland, 1990.

[27] J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill, “Sequential circuit

65

verification using symbolic model checking”, In 27th ACM/IEEE Design Automation Conference, 1990.

[28] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang, “Symbolic model checking: 10E20 states and beyond”, In LICS, 1990.

[29] K. L. McMillan, “Symbolic model checking - an approach to the state explosion problem” PhD thesis, SCS, Carnegie Mellon University, 1992.

[30] E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, L.

A. Ness, “Verification of the Futurebus+ cache coherence protocol”, In L.

Claesen, Proceedings of the Eleventh International Symposium on Computer Hardware Description Languages and their Applications. North-Holland, April 1993.

[31] E. M. Clarke, O. Grumberg, D. E. Long, “Model checking and abstract”, ACM Symposium on Principles of Programming Languages, January 1992.

[32] E. M. Clarke, E. A. Emerson and A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications”, In ACM Trans. on Programming Languages and Systems, 8(2):244--263, 1986.

[33] Getting start with SMV tutorial, K. L. McMillan, Cadence Berkeley Labs 2001, http://www.cs.indiana.edu/classes/p515/readings/smv/CadenceSMV-docs/smv/tu torial/tutorial.html

[34] Steven J. Leon, LINEAR ALGEBRA WITH APPLICATIONS, Prentice Hall, 2002 [35] William Ford, William Topp, DATA STRUCTURES with C++ using STL,

Prentice Hall, 2002

[36] E. M. Clarke and E. A. Emerson, Synthesis of synchronization skeletons for branching time temporal logic, In Logic of Programs: Workshop, Yorktown Heights, NT, May 1981, volume 131 of Lecture Notes in Computer Science.

Springer-Verlag, 1981

[37] E. A. Emerson and J. Y. Halpern, “Sometimes” and “Not Never” revisited: On branching time versus linear time, Journal of the ACM, 33:151-178, 1986

[38] 洪維恩, C++教學手冊(第二版), 博碩文化, April 2006 [39] 洪錦魁, 精通C語言, 文魁資訊股份有限公司, March 2002 [40] Advanced Microcontroller Bus Architecture Specification

[41] Bloem R., Ravi K., Somenz F., “Symbolic guided search for CTL model checking”, Design Automation Conference, pp.:29 – 34, June 2000

[42] ARM Powered Training documentation

[43] .NET Framework Developer Center, ASP.NET Technical Articles, Finite State Machines, Wizards, and the Web

http://msdn2.microsoft.com/en-us/library/aa478972.aspx

67