Architecture transformations are frequently performed during software design and maiatenance. However this activity is not well supported at a sufficiently abstract level. In this paper, the authors characterize archi...Architecture transformations are frequently performed during software design and maiatenance. However this activity is not well supported at a sufficiently abstract level. In this paper, the authors characterize architecture transformations using graph rewriting rules, where architectures are represented in graph notations. Architectures are usually required to satisfy certain constraints during evolution. Therefore a way is presented to construct the suffi- cient and necessary condition for a transformation to preserve a constraint. The condition can be verified before the application of the transformation. Validated transformations are guaranteed not to violate corresponding constraints whenever applied.展开更多
Can the semantics of a program be represented as a single formula? We show that one formula is insufficient to handle assertions, refinement or slicing, while two formulae are sufficient: A (S) , defining non-terminat...Can the semantics of a program be represented as a single formula? We show that one formula is insufficient to handle assertions, refinement or slicing, while two formulae are sufficient: A (S) , defining non-termination, and B (S), defining behaviour. Any two formulae A and B will define a corresponding program. Refinement is defined as implication between these formulae.展开更多
首先给出了量子最弱自由前置条件(weakest liberal precondition,简称wlp)wlp(A,B,C)-可交换的定义,研究了wlp(A,B,C)-可交换的充分必要条件;其次,得到了wlp不是良好的谓词转换,验证了wlp是比量子最弱前置条件(weakest precondition,简...首先给出了量子最弱自由前置条件(weakest liberal precondition,简称wlp)wlp(A,B,C)-可交换的定义,研究了wlp(A,B,C)-可交换的充分必要条件;其次,得到了wlp不是良好的谓词转换,验证了wlp是比量子最弱前置条件(weakest precondition,简称wp)更弱的谓词转换,揭示了wlp和wp的本质区别;最后证明了wlp的序列合成、并行合成和块结构等性质.展开更多
This work is focused on presenting a split precondition approach for the modeling and proving the correctness of distributed algorithms. Formal specification and precise analysis of Peterson's distributed mutual e...This work is focused on presenting a split precondition approach for the modeling and proving the correctness of distributed algorithms. Formal specification and precise analysis of Peterson's distributed mutual exclusion algorithm for two process has been considered. The proof of properties like, mutual exclusion, liveness, and lockout-freedom have also been presented. Keywords distributed algorithms - state transition rule - mutual exclusion - weakest self-precondition - weakest co-operation - correctness Regular PaperAwadhesh Kumar Singh received the B.E. degree in computer science & engineering from Gorakhpur University, Gorakhpur, India in 1988. He received the M.E. and Ph.D. (Engg) degrees in the same area from Jadavpur University, Kolkata, India. He is a faculty member in Computer Engineering Department, National Institute of Technology, Kurukshetra, India. His present research interest is distributed systems.Anup Kumar Bandyopadhyay received the B.E. (Tel.E.), M.E. (Tel.E.), and Ph.D. (Engg) degrees from Jadavpur University, Calcutta, India in 1968, 1970 and 1983, respectively. From 1970 to 1972 he worked with the Microwave Antenna System Engineering Group of the Indian Space Research Organization. In 1972 he joined the Department of Electronics and Telecommuication Engineering, Jadavpur University, where he is currently a professor. His research interests include computer communication networks and distributed systems.展开更多
基金This work was supported by the National Natural Science Foundation of China (No.69773025) and Ph.D. Foundationof the Ministry
文摘Architecture transformations are frequently performed during software design and maiatenance. However this activity is not well supported at a sufficiently abstract level. In this paper, the authors characterize architecture transformations using graph rewriting rules, where architectures are represented in graph notations. Architectures are usually required to satisfy certain constraints during evolution. Therefore a way is presented to construct the suffi- cient and necessary condition for a transformation to preserve a constraint. The condition can be verified before the application of the transformation. Validated transformations are guaranteed not to violate corresponding constraints whenever applied.
文摘Can the semantics of a program be represented as a single formula? We show that one formula is insufficient to handle assertions, refinement or slicing, while two formulae are sufficient: A (S) , defining non-termination, and B (S), defining behaviour. Any two formulae A and B will define a corresponding program. Refinement is defined as implication between these formulae.
文摘首先给出了量子最弱自由前置条件(weakest liberal precondition,简称wlp)wlp(A,B,C)-可交换的定义,研究了wlp(A,B,C)-可交换的充分必要条件;其次,得到了wlp不是良好的谓词转换,验证了wlp是比量子最弱前置条件(weakest precondition,简称wp)更弱的谓词转换,揭示了wlp和wp的本质区别;最后证明了wlp的序列合成、并行合成和块结构等性质.
文摘This work is focused on presenting a split precondition approach for the modeling and proving the correctness of distributed algorithms. Formal specification and precise analysis of Peterson's distributed mutual exclusion algorithm for two process has been considered. The proof of properties like, mutual exclusion, liveness, and lockout-freedom have also been presented. Keywords distributed algorithms - state transition rule - mutual exclusion - weakest self-precondition - weakest co-operation - correctness Regular PaperAwadhesh Kumar Singh received the B.E. degree in computer science & engineering from Gorakhpur University, Gorakhpur, India in 1988. He received the M.E. and Ph.D. (Engg) degrees in the same area from Jadavpur University, Kolkata, India. He is a faculty member in Computer Engineering Department, National Institute of Technology, Kurukshetra, India. His present research interest is distributed systems.Anup Kumar Bandyopadhyay received the B.E. (Tel.E.), M.E. (Tel.E.), and Ph.D. (Engg) degrees from Jadavpur University, Calcutta, India in 1968, 1970 and 1983, respectively. From 1970 to 1972 he worked with the Microwave Antenna System Engineering Group of the Indian Space Research Organization. In 1972 he joined the Department of Electronics and Telecommuication Engineering, Jadavpur University, where he is currently a professor. His research interests include computer communication networks and distributed systems.
