Equivalence Checking of Java']Java Methods - Toward Ensuring IoT Dependability -

被引:0
|
作者
Okano, Kozo [1 ]
Harauchi, Satoshi [2 ]
Sekizawa, Toshifusa [3 ]
Ogata, Shinpei [1 ]
Nakajima, Shin [4 ]
机构
[1] Shinshu Univ, Fac Engn, 4-17-1 Wakasato, Nagano 3808553, Japan
[2] Mitsubishi Electr Corp, Adv Technol R&D Ctr, 8-1-1 Tsukaguchi Honmachi, Amagasaki, Hyogo 6618661, Japan
[3] Nihon Univ, Coll Engn, 1 Tamuramachi Tokusada, Koriyama, Fukushima 9638642, Japan
[4] Natl Inst Informat, Chiyoda Ku, 2-1-2 Hitotsubashi, Tokyo 1018430, Japan
关键词
software verification; !text type='Java']Java[!/text; hash code; and equivalence; VERIFICATION;
D O I
暂无
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
IoT devices are software-rich and Java is sometimes chosen as the developing programming language. Although Java is highly productive in constructing large advanced programs, application or user-defined Java classes must be responsible for safety and security issues. In particular, two fundamental methods hashCode and equals play key roles in safety and security assurance. Some existing studies for ensuring the correctness of these two methods rely on static analysis, which are limited to loop-free programs only. This paper proposes a new solution to this important problem, based on equivalence checking of methods or functions. The proposed approach makes use of software analysis workbench (SAW), an open source tool. The approach is also useful in reducing the cost of regression testing when program refactoring is conducted.
引用
收藏
页数:6
相关论文
共 50 条
  • [1] Java']Java model checking
    Park, DYW
    Stern, U
    Skakkebæk, JU
    Dill, DL
    FIFTEENTH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2000, : 253 - 256
  • [2] Extended static checking for Java']Java
    Nelson, G
    MATHEMATICS OF PROGRAM CONSTRUCTION, PROCEEDINGS, 2004, 3125 : 1 - 1
  • [3] Extended Static Checking for Java']Java
    Flanagan, Cormac
    Leino, K. Rustan M.
    Lillibridge, Mark
    Nelson, Greg
    Saxe, James B.
    Stata, Raymie
    ACM SIGPLAN NOTICES, 2013, 48 (04) : 22 - 33
  • [4] Extended static checking for Java']Java
    Flanagan, C
    Leino, KRM
    Lillibridge, M
    Nelson, G
    Saxe, JB
    Stata, R
    ACM SIGPLAN NOTICES, 2002, 37 (05) : 234 - 245
  • [5] Java']Java Virtual Machine monitoring for dependability benchmarking
    Orlando, Salvatore
    Russo, Stefano
    NINTH IEEE INTERNATIONAL SYMPOSIUM ON OBJECT AND COMPONENT-ORIENTED REAL-TIME DISTRIBUTED COMPUTING, PROCEEDINGS, 2006, : 433 - 440
  • [6] Ensuring the Integrity of Running Java']Java Programs
    Thober, Mark A.
    Pendergrass, J. Aaron
    Jurik, Andrew D.
    JOHNS HOPKINS APL TECHNICAL DIGEST, 2013, 32 (02): : 517 - 527
  • [7] Model checking real time Java']Java using Java']Java PathFinder
    Lindstrom, G
    Mehlitz, PC
    Visser, W
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2005, 3707 : 444 - 456
  • [8] Model checking the Java']Java metalocking algorithm
    Basu, Samik
    Smolka, Scott A.
    ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2007, 16 (03) : C1 - C35
  • [9] Model checking programs with Java']Java PathFinder
    Visser, W
    Mehlitz, P
    MODEL CHECKING SOFTWARE, PROCEEDINGS, 2005, 3639 : 27 - 27
  • [10] Applying model checking in Java']Java verification
    Havelund, K
    Skakkebæk, JU
    THEORETICAL AND PRACTICAL ASPECTS OF SPIN MODEL CHECKING, 1999, 1680 : 216 - 231