Formal Description of Software Dynamic Correctness

Ma Yanfang; Zhang Min; Chen Yixiang

Journal of Computer Research and Development > 2013 > 50(3): 626-635.

Ma Yanfang, Zhang Min, Chen Yixiang. Formal Description of Software Dynamic Correctness[J]. Journal of Computer Research and Development, 2013, 50(3): 626-635.

Citation:

Ma Yanfang, Zhang Min, Chen Yixiang. Formal Description of Software Dynamic Correctness[J]. Journal of Computer Research and Development, 2013, 50(3): 626-635.

Citation:

Ma Yanfang, Zhang Min, Chen Yixiang. Formal Description of Software Dynamic Correctness[J]. Journal of Computer Research and Development, 2013, 50(3): 626-635.

PDF (1045 KB)

Formal Description of Software Dynamic Correctness

1(School of Computer Science and Technology, Huaibei Normal University, Huaibei, Anhui 235000) 2(Shanghai Key Laboratory of Trustworthy Computing (Software Engineering Institute, East China Normal University), Shanghai 200062)

More Information

Published Date: March 14, 2013

Graphical Abstract

Abstract

Abstract

Correctness is a key attribute of software trustworthiness. Abstractly, software correctness can be represented as whether or not the implementation of software satisfies its specification. However, in the real world, it is difficult to get the satisfaction absolutely. In the course of developing and designing software, implementation is often modified in order to satisfy its specification. This means that the software is more and more close to correctness, i.e. software correctness is a dynamic course. In order to describe the dynamic correctness of software, in this paper, the abstract characterization and the limit theory of dynamic correctness based on parameterized bisimulation are proposed. Firstly, the infinite evolution mechanism of parameterized bisimulation is established. Parameterized limit bisimulation is defined in order to characterize the relation between a series of software implementations obtained in the real design and its specification, and some special examples are shown. Secondly, parameterized bisimulation limit is given, and the recursive characterization of parameterized bisimulation limit is stated. Finally, some algebraic properties are proved, such as the uniqueness of parameterized bisimulation limit and the consistence between parameterized bisimulation limit and parameterized bisimulation.
- correctness of software,
- parameterized bisimulation,
- formalization,
- limit,
- topology

FullText(HTML)

References (0)

[1]	Fu Tao, Chen Zhaojiong, Ye Dongyi. GAN-Based Bidirectional Decoding Feature Fusion Extrapolation Algorithm of Chinese Landscape Painting[J]. Journal of Computer Research and Development, 2022, 59(12): 2816-2830. DOI: 10.7544/issn1000-1239.20210830
[2]	Guo Sixu, He Shen, Su Li, Zhang Xing, Zhou Fucai, Zhang Xinyue. Top-k Boolean Searchable Encryption Scheme Based on Multiple Keywords[J]. Journal of Computer Research and Development, 2022, 59(8): 1841-1852. DOI: 10.7544/issn1000-1239.20200605
[3]	Jiang Bin, Liu Hongyu, Yang Chao, Tu Wenxuan, Zhao Zilong. A Face Inpainting Algorithm with Local Attribute Generative Adversarial Networks[J]. Journal of Computer Research and Development, 2019, 56(11): 2485-2493. DOI: 10.7544/issn1000-1239.2019.20180656
[4]	Guo Yingjie, Liu Xiaoyan, Wu Chenxi, Guo Maozu, Li Ao. U-Statistics and Ensemble Learning Based Method for Gene-Gene Interaction Detection[J]. Journal of Computer Research and Development, 2018, 55(8): 1683-1693. DOI: 10.7544/issn1000-1239.2018.20180365
[5]	Zhang Peng, Duan Lei, Qin Pan, Zuo Jie, Tang Changjie, Yuan Chang’an, Peng Jian. Mining Top-k Distinguishing Sequential Patterns Using Spark[J]. Journal of Computer Research and Development, 2017, 54(7): 1452-1464. DOI: 10.7544/issn1000-1239.2017.20160553
[6]	Li Bohan, Zhang Chao, Li Dongjing, Xu Jianqiu, Xia Bin, Qin Xiaolin. A DSP-Topk Query Optimization Algorithm Supporting Indoor Obstacle Space[J]. Journal of Computer Research and Development, 2017, 54(3): 557-569. DOI: 10.7544/issn1000-1239.2017.20150895
[7]	Zhang Jianfeng, Han Weihong, Fan Hua, Zou Peng, Jia Yan. An Algorithm for Top-k Query Refinement Based on User’s Feedback[J]. Journal of Computer Research and Development, 2014, 51(10): 2206-2215. DOI: 10.7544/issn1000-1239.2014.20130827
[8]	Jiang Tao, Zhang Bin, Gao Yunjun, Yue Guangxue. Efficient Top-k Query Processing on Mutual Skyline[J]. Journal of Computer Research and Development, 2013, 50(5): 986-997.
[9]	Wang Shuang, Wang Guoren. Sliding Window Top-K Frequent Item Query on Uncertain Stream[J]. Journal of Computer Research and Development, 2012, 49(10): 2189-2197.
[10]	Xiong Gangqiang, Yu Jiande, Xiong Changzhen, Qi Dongxu. Reversible Factorization of U Orthogonal Transform and Image Lossless Coding[J]. Journal of Computer Research and Development, 2012, 49(4): 856-863.