VERIFICATION PROPERTY INTEGRATION DEVICE, VERIFICATION PROPERTY INTEGRATION METHOD, AND RECORDING MEDIUM HAVING VERIFICATION PROPERTY INTEGRATION PROGRAM STORED THEREIN

WIPO Patent Application WO/2015/159501

A1

Provided are a verification property integration device, a verification property integration method, and a verification property integration program that enable verification of a product or system coupling products verified by different formal techniques, such as by formal specification description or model inspection. A verification property integration device includes: a library (13) defining the semantics of formal specification description and model inspection description given with respect to a theorem proof assist-system description; a first theorem proof assist-system description generation unit (11) that converts, using the library (13), the formal specification description to an expression in terms of a theorem proof assist system; and a second theorem proof assist-system description generation unit (12) that converts, using the library (13), a model in the model inspection description and a temporal logic formula to an expression in terms of the theorem proof assist system.

JIANG FAN (JP)

PCT/JP2015/001924

October 22, 2015

April 06, 2015

Click for automatic bibliography generation  

NEC CORP (JP)

G06F9/44; G06F11/36

AKITOSHI TAKAYA: "Inter-Model Consistency between UML Class and Sequence Models", IEICE TECHNICAL REPORT, vol. 109, no. 298, 20 November 2009 (2009-11-20), pages 25 - 30
NAOYASU UBAYASHI: " Formal Methods-Bases and Applications", SYSTEMS, CONTROL AND INFORMATION, vol. 52, no. 9, 15 September 2009 (2009-09-15), pages 8 - 13
HIRONOBU KURUMA: "Sentan Software Tool", COMPUTER SOFTWARE, vol. 24, no. 2, 24 April 2007 (2007-04-24), pages 21 - 48

SHIMOSAKA, NAOKI (JP)
Naoki Shimosaka (JP)

View/Download PDF      PDF Help

Previous Patent: HEAD-UP DISPLAY DEVICE

Next Patent: WINDOW OPENING-CLOSING DEVICE