An experiment in parallelizing an application using formal methods -: Computer aided parallelization

被引：0
|
作者：
Couturier, R [1 ]
Méry, D [1 ]
机构：
[1] Univ Nancy 1, UMR 7503 LORIA CNRS, F-54506 Vandoeuvre Nancy, France
来源：
COMPUTER AIDED VERIFICATION | 1998年 / 1427卷
关键词：
D O I：
暂无
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
Scientists and engineers have successfully developed much useful sequential code using classical programming languages, such as Fortran, and highly performant computers can help them to model problems whilst improving their results of simulation. However, great skill and care are required to design correct parallel code from sequential code. We focus our work on 3 aspects of producing correct parallel code from sequential code. First, we use a theorem prover, namely PVS, as a practical tool for asserting proof obligations and for stating programs and properties. Secondly, we build an abstraction from some sequential code in order to derive a postcondition. Finally, we characterize the "glueing condition" that will ensure the correctness of the final parallel code. Our method does not need any new notation but reuses proof theoretical notations together with the composition of postconditions with respect to the glueing condition.
引用
收藏
页码：345 / 356
页数：12
相关论文
共 50 条
  • [21] STUDENT ANTENNA EXPERIMENT USING COMPUTER AIDED DESIGN AND TEST.
    Owen, Earl F.
    Braithwaite, Kent
    Buttars, David B.
    Erdman, James R.
    CoED, 1988, 8 (01): : 28 - 30
  • [22] A case study on applying formal methods to medical devices: Computer-aided resuscitation algorithm
    Jetley R.P.
    Carlos C.
    Iyer S.P.
    International Journal on Software Tools for Technology Transfer, 2004, 5 (04) : 320 - 330
  • [23] Application of Computer Aided Tools and Methods for Unmanned Cargo Aircraft Design
    Czyba, Roman
    Hecel, Micha
    Jablonski, Karol
    Lemanowicz, Marcin
    Platek, Krzysztof
    2015 20TH INTERNATIONAL CONFERENCE ON METHODS AND MODELS IN AUTOMATION AND ROBOTICS (MMAR), 2015, : 1068 - 1073
  • [24] Methods for parallelizing the Probabilistic Neural Network on a Beowulf cluster computer
    Secretan, Jimmy
    Georgiopoulos, Michael
    Maidhof, Ian
    Shibly, Philip
    Hecker, Joshua
    2006 IEEE INTERNATIONAL JOINT CONFERENCE ON NEURAL NETWORK PROCEEDINGS, VOLS 1-10, 2006, : 2378 - +
  • [25] Computer Aided Flowsheet Design using Group Contribution Methods
    Bommareddy, Susilpa
    Eden, Mario R.
    Gani, Rafiqul
    21ST EUROPEAN SYMPOSIUM ON COMPUTER AIDED PROCESS ENGINEERING, 2011, 29 : 321 - 325
  • [26] Application of the formal model for describing processes of adaptive information security in computer-aided systems
    F. G. Nesteruk
    L. G. Nesteruk
    G. F. Nesteruk
    Automation and Remote Control, 2009, 70 : 491 - 501
  • [27] Application of the formal model for describing processes of adaptive information security in computer-aided systems
    Nesteruk, F. G.
    Nesteruk, L. G.
    Nesteruk, G. F.
    AUTOMATION AND REMOTE CONTROL, 2009, 70 (03) : 491 - 501
  • [28] Towards a formal model of visual design aided by computer
    Grabska, E.J.
    Grabska, E.J. (ewa.grabska@uj.edu.pl), 1600, Springer Verlag (98): : 135 - 147
  • [29] Towards a Formal Model of Visual Design Aided by Computer
    Grabska, E. J.
    HUMAN-COMPUTER SYSTEMS INTERACTION: BACKGROUNDS AND APPLICATIONS 2, PT 1, 2012, 98 : 135 - 147
  • [30] Computer-aided experiment on arc welding
    Ohji, Takayoshi
    Welding International, 2009, 23 (01) : 21 - 26
12345