TY - JOUR
T1 - Formal approach to assertion-based code generation
AU - Li, Pengyi
AU - Sun, Jing
AU - Wang, Hai
PY - 2017/11/1
Y1 - 2017/11/1
N2 - With the growing in size and complexity of modern computer systems, the need for improving the quality at all stages of software development has become a critical issue. The current software production has been largely dependent on manual code development. Despite the slow development process, the errors introduced by the programmers contribute to a substantial portion of defects in the final software product. This paper investigates the synergy of generating code and assertion constraints from formal design models and use them to verify the implementation. We translate Z formal models into their OCL counterparts and Java assertions. With the help of existing tools, we demonstrate various checkings at different levels to enhance correctness.
AB - With the growing in size and complexity of modern computer systems, the need for improving the quality at all stages of software development has become a critical issue. The current software production has been largely dependent on manual code development. Despite the slow development process, the errors introduced by the programmers contribute to a substantial portion of defects in the final software product. This paper investigates the synergy of generating code and assertion constraints from formal design models and use them to verify the implementation. We translate Z formal models into their OCL counterparts and Java assertions. With the help of existing tools, we demonstrate various checkings at different levels to enhance correctness.
KW - formal specification
KW - verification and validation
KW - simulation
KW - Java assertions
UR - https://www.scopus.com/record/display.uri?eid=2-s2.0-85041173402&origin=SingleRecordEmailAlert&dgcid=raven_sc_search_en_us_email&txGid=dafabb90b1148e4087131191f5475a32
UR - https://www.worldscientific.com/doi/abs/10.1142/S0218194017400162
U2 - 10.1142/S0218194017400162
DO - 10.1142/S0218194017400162
M3 - Article
SN - 0218-1940
VL - 27
SP - 1637
EP - 1662
JO - International Journal of Software Engineering and Knowledge Engineering
JF - International Journal of Software Engineering and Knowledge Engineering
IS - 09n10
ER -