Proving correctness of transformation functions in real-time groupware

被引:0
|
作者
Imine, A
Molli, P
Oster, G
Rusinowitch, M
机构
关键词
D O I
暂无
中图分类号
G2 [信息与知识传播];
学科分类号
05 ; 0503 ;
摘要
Operational transformation is an approach which allows to build real-time groupware tools. This approach requires correct transformation functions. Proving the correction of these transformation functions is very complex and error prone. In this paper, we show how a theorem prover can address this serious bottleneck. To validate our approach, we have verified the correctness of state-of-art transformation functions defined on Strings with surprising results.. Counter-examples provided by the theorem prover have helped us to define new correct transformation functions for Strings.
引用
收藏
页码:277 / 293
页数:17
相关论文
共 50 条
  • [1] USING A REAL-TIME GROUPWARE IN THE EDUCATIONAL PROCESS
    Smutny, Pavel
    PROCEEDINGS OF 11TH INTERNATIONAL CARPATHIAN CONTROL CONFERENCE, 2010, 2010, : 53 - 56
  • [2] Proving properties of real-time semaphores
    Univ of York
    Sci Comput Program, 2 (159-181):
  • [3] PROVING PROPERTIES OF REAL-TIME SEMAPHORES
    SCHOLEFIELD, D
    SCIENCE OF COMPUTER PROGRAMMING, 1995, 24 (02) : 159 - 181
  • [4] Adaptive Forward Error Correction for Real-Time Groupware
    Dyck, Jeff
    Gutwin, Carl
    Makaroff, Dwight
    PROCEEDINGS OF THE 17TH ACM INTERNATIONAL CONFERENCE ON SUPPORTING GROUP WORK, 2012, : 121 - 130
  • [5] A descriptive framework of workspace awareness for real-time groupware
    Gutwin C.
    Greenberg S.
    Computer Supported Cooperative Work (CSCW), 2002, 11 (3-4): : 411 - 446
  • [6] Correctness of efficient real-time model checking
    Reif, W
    Schellhorn, G
    Vollmer, T
    Ruf, J
    JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2001, 7 (02) : 194 - 209
  • [7] Correctness of real-time transactions and its implementation
    Li, G.H.
    Liu, Y.S.
    Jisuanji Yanjiu yu Fazhan/Computer Research and Development, 2001, 38 (09):
  • [8] Implementation Correctness of a Real-Time Operating System
    Daum, Matthias
    Schirmer, Norbert W.
    Schmidt, Mareike
    SEFM 2009: SEVENTH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2009, : 23 - +
  • [9] Relaxing correctness criteria in real-time DBMSs
    Sadeg, B
    Saad-Bouzefrane, S
    COMPUTERS AND THEIR APPLICATIONS, 2000, : 64 - 67
  • [10] An intelligent groupware environment for real-time distributed medical collaboration
    Gong, LG
    Kulikowski, CA
    Chang, SM
    JOURNAL OF THE AMERICAN MEDICAL INFORMATICS ASSOCIATION, 1997, : 959 - 959