中文模板

Size: px

Start display at page:

Download "中文模板"

副线
4 years ago
Views:

1 -98//33- Joural of Software Vol3 No Ada 79 9 E-mal cjjag@oleshc http//wwwsdusteduc Ada Ada Ada Ada Ada Ada P3 A Petr [] Ada [3] Petr Petr Petr Petr 3 Ada [4] [] [6] [7] [8] [6] Ada AA G DJ Petr 96 Petr

2 36 Joural of Software 3 HRG HRG Petr Ada Ada Petr [9] [~3] Petr [4] PV N S F N S F N N S S S S S 3 F F F N Petr N s s s S N Petr - N S F N S F N N N - S S S S j j S S j j j 3 F F F F N j N Petr N s s s S - Petr 3R- R- V E L v V E L E Petr R- R- R- 4G- RG RG RG R- RG V E L v R- RG RG RG G- RG RG RG R- RG V E L v V E L v V V V V v v v 3 v 4 V E L a v V b v v v V V V v v v v V t { } v v L v v t t v v v v v v V v v E L v v t v

3 Ada 37 c V E L RG t 3 t v a b V E L v R- a b t RG RG R- RG V E L v c v v 3 t t v v v v t t 4 v v a RG b RG c G-CombeRG RG Fg t v 3 v t v v t v 3 v t 4 t 3 G- RG v v v 3 v t 4 v v Ada - Petr - Petr - Petr S F Petr Petr S F L Γ L Γ L [] S F Petr - Petr S F L Γ L Γ L Γ L L Γ L Γ L S F Petr - Petr S F L Γ L Γ L Γ L + - Petr + L L +- Petr + + L Γ + L Γ + L Γ + + Γ + L Γ L Γ L + Γ + L Γ + L Γ + + Γ + + L L Γ L Ada Petr [] Ada Ada Ada Petr Ada Ada + t 3

4 38 Joural of Software 3 f-elsecase loop Ada Ada Petr [~3] Ada a Ada Petr etry b Ada Petr c Ada etry ac-etry etry etry-beg ac-etry ac- etry-ex beg- ed- -doe etry-beg ac-etry wat-ac etry-ex ac- beg- ed- -doe etry-ed ac- etry-ed a b c Fg Ada ac-etryetry-exac- -doe -doe Ada Ada [478] Ada Ada 3 tas body Customer s beg 3 loop 4 OperatorPrepay PumpStart 6 PumpFsh 7 Chage 8 ed loop 9 ed Customer tas body Pump s beg loop 3 Actvate 4 Start Fsh do 6 OperatorCharge 7 ed Fsh 8 ed loop 9 ed Pump tas body Operator s beg loop 3 select 4 Prepay do PumpActvate 6 ed Prepay 7 or 8 Charge do 9 CustomerCharge 3 ed Charge 3 ed select 3 ed loop 33 ed Operator Ada [~4] Ada Petr

5 Ada 39 Ada 3 Ada 4 Ifcase Ada beg--operator beg--customer t loop- t 3 t loop-3 t t 33 t select-3 beg--pump etry-o-4 t t 3 etry-p- loop- ac-etry-o-4 t 4 t -3 ac-etry-p- wat-ac-o-4 etry-ex-4-4 t 3 wat-ac-p- t 4 ac--o-4 t 6 t ac--p- ed--6-4 ed-select-3 etry-p- t 3 ed-loop-3 t t wat-ac-p- ac-etry-p- t 4 t 6 etry-p-6 ac--p- - t 7 t 8 t 9 ed-loop-8 wat-ac-p-6-7 t ac-etry-p-6 t 9 etry-o-6 t 6 ac-etry-o-6 ac-etry-c-9 wat-ac-o-6 etry-ex-8-6 ac--c-9 ac--o-6 etry-ex--6 ed- -7 ac--p-6 t 7 t 8 t 8 t 3 etry-c-9 t 9 wat-ac-c-9 t 3 ed--3 Fg3 Ada et of source program ed-loop-8 3 Ada Ada Ada Ada -doe 3 Ada 4a 4b c

6 3 Joural of Software 3 Ada etry-beg etry ac-etry wat-ac etry-ex ac- ed- a b Fg4 4 3 Ada as customer ac- etry-ed beg--customer -doe -doe t loop-3 t etry-o-4 t 3 wat-ac-o-4 t 4 etry-p- ac-etry-o-4 ac--o-4 ac-etry-p- t 3 etry-ex-4-4 t 6 3 as Customer loop- beg--operator t t t t wat-ac-p- t 4 t 3 etry-p- select-3 t 8 etry-c-9 t 6 etry-p-6 t 7 wat-ac-p-6 t 8-7 t 9 ac--p- ac-etry-p-6 ac--p-6 ed-loop-8 t etry-ex--6 t 8 t 3 ac-etry-p- wat-ac-p- t 4 t 9 t t 3 ed-loop-3 t 3 ac-etry-c-9 wat-ac-c-9 ac--p- ac--c-9 ed--6 ed--3 ed-select-3 t 33 t 6 t 3 t 9 a Fg b

7 Ada 3 as Pump beg--pump t loop- t -3 a s t t t 3 a t 3 a 3 t 6 a b c s a b c s a b c s4 8 a b c s s a b c s 4 s s s 9 c a b s s a b c a b c t 3-4 a 4 s t 4 t t 3 3 a3 b c3 t 4 3 a3 b c4 s 4 t 3 t 9 t 6 t 4 - t etry-o-6 ac-etry-o-6 t 8 a t 4 t a 6 s 3 t 6 t 7 a 7 t s 4 4 a3 b c3 t 4 t 3 a3 b c4 6 a3 c s 4 wat-ac-o-6 etry-ex- 8-6 a 8 t 8 t 7 a3 c6 t 7 ac--o-6 ed- -7 t 8 ed-loop-8 t 3 a 9 t8 a t 9 a t 6 8 a4 c7 s 9 a c7 s 6 s 6 4 a4 c s Fgc Fg6 a RG c 6 a RG t 3 c c 3 c s t t t 9 b b s 4 t t t 8 a a c t4 s c t 4 a6 b4 c s 3 3 a7 b4 c a c s s 6 t 3 t 33 t 4 c 4 t 3 c t c 6 t 6 t 8 c 8 t 9 c 9 t 9 c t 3 c t 3 s 6 b t 3 b 3 t 4 b 4 t b t 6 b 9 t t 7 4 a8 b c a b 8 t 6 t 3 b 7 t 8 b 6 a8 b6 c t a8 b7 c9 t 9 7 a8 b7 c 4 a 3 b c 3 a 3 c 7 c Fg6b RG 3 Fg6c RG Fg7 6b RG 3 6c RG Ada 7 RG ~ α α j j

8 3 Joural of Software 3 + s + ss + ss4s + s4 ss ss t3 s + s4st ss + ss + ss4s + ss4s + s4 ss ss t3 + t3 3 s4t3 4 3 s4 4 t4s4 4 t4 + 3 ss + ss t3s4t4 + ss + ss s4 + ss4s + ss4s + s4 ss + ss t3t4 ss + ss s4 + ss4s + ss4s + s4 ss + ss t3t4 + s + ss t3s4t4 s s t s t + s s s t t t3tt6 s s6 t4 s s3tt6t8t97 4 s s s t3s4t4 + s s4 s t3t4 t3 tt6 s s6 t4 s s3tt6t8t97 s t t t t t t t t t + t t t t t t t t t t t t t t t t t t t t t t t t t Ada Ada S F 4 S s S ttt3 tt t3ttt4 + ttt3 tt tt t3t4 t3 tt6 t4t t3t33 t4 tt t6t7tt6t8t9 s S { beg Customer beg Pump beg Operator} L L 4 Ada Petr 4 Ada Ada Ada []

9 Ada 33 [] Petr σ & σ { x x σ } 6 L pref L { σ L σ σ o σ L} spref L { σ L σ σ o σ L σ } stpref L { σ L σ σ o σ L & σ } pref L spref L stpref L L 3 Petr PN S F PN L PN spref L PN [] 3 Ada Ada S F S s Ada L spref L s S Ada 4 Ada Ada S F S s S s t ed Ada σ L σ σ o t σ σ o σ L t t ed t ed σ σ o t σ σ o σ L t ed t t ed 4 4 Ada 4Ada Deadloc-Aalyss σ L σ σ o σ L σ False rue beg whle σ t f t t ed the { } rue elsef t the { } False edf eddo edbeg t t t 7 6 9

10 34 Joural of Software 3 Ada Customer Pump Fsh Pump Fsh OperatorCharge Operator Charge CustomerCharge Customer PumpFsh 4 7 Ada Ada Petr PN S F PN L PN stpref L PN [] Ada Ada S F S [] s Ada L stpref L s S 6 Ada Ada SF S s S s Ada σ L σ α o β t t &β σ σ o σ L σ L σ α o β t t &β σ σ oσ L 6Ada Lveloc-Aalyss σ L σ σ o σ L σ False rue beg f σ β the { } 3 rue 4 else for to Legth β do 6 σ t 7 f t the 8 edfor t { t } 9 f the { } False else { } rue 3 edf

11 Ada 3 4 edf edbeg Petr Ada Ada Refereces [] Shatz S Cheg WK A Petr et framewor for automated statc aalyss of Ada tas behavor Joural of System ad Software ~39 [] urata Sheer B Shatz S Detecto of Ada statc deadlocs usg Petr et varats IEEE rasactos o Software Egeerg ~36 [3] Shatz S a K Blac C et al Desg ad mplemetato of a Petr et-based toot for Ada tasg aalyss IEEE rasactos o Parallel ad Dstrbuted System 99444~44 [4] Shatz S u Sheg-ru urata A applcato of Petr et reducto for Ada tasg deadloc aalyss IEEE rasactos o Parallel ad Dstrbuted Systems ~3 [] Godefrod P Wolper P Usg partal orders for the effcet verfcato of deadloc freedom ad safety propertes Formal ethods System Desg 99349~64 [6] Notom urata Herarchcal reachablty graph of bouded Petr ets for cocurret-software IEEE rasactos o Software Egeerg 9943~336 [7] Dur S Buy U Devwapall R et al Usg state space reducto methods for deadloc aalyss Ada tasg I Proceedgs of the 993 Iteratoal Symposum o Software estg ad Aalyss New Yor NY AC Press 993 ~6 [8] Corbett JC Evaluatg deadloc detecto methods for cocurrecy software IEEE rasactos o Software Egeerg 99636~8 [9] Peterso JL Petr Net heory ad the odelg of Systems Eglewood Clffs Pretce-Hall 98 [] urata Petr ets properter aalyss ad applcatos Proceedgs of the IEEE ~8 [] Jag Chag-ju PN ache heores of Dscrete Evet Systems Bejg Scece Press Chese [] Jag Chag-ju Dyamc varace of Petr et Scece Cha Seres E ~73 Chese [3] Jag Chag-ju Complete sequece behavor varace of sychroous composto ets Joural of Appled Scece 837~7 Chese [4] Jag Chag-ju Zhag Zhao-qg Qao Ru-lag he desg of parallel program based o PN mache Hgh echology Letters 99888~3 Chese

12 36 Joural of Software 3 [] Baraou K Verfcato cocurret programmg wth Petr ets structural techques I Proceedgs of the 3rd Iteratoal IEEE Hgh Assurace System Egeerg Symposum 998 4~33 IEEE Computer Socety Press 998 4~33 http// www computerorg/proceedgs/hase/9/9tochtm [] PN [] Petr E ~73 [3] 837~7 [4] PN 99888~3 Aalyss ad Verfcato of Local Propertes of Ada asg Based o Net Laguage DING Zh-ju JIANG Chag-ju Collage of Iformato Scece ad Egeerg Shadog Uversty of Scece ad echology aa 79 Cha Departmet of Computer Scece ad Egeerg ogj Uversty Shagha 9 Cha E-mal cjjag@oleshc http//wwwsdusteduc Abstract I ths paper the propertes of Ada tasg ad the correlatve state exploso problem are dscussed by usg the et laguage he sychroous composto ad decomposto of Ada et s studed as a result et laguage propertes are obtaed ad the safeess ad lveess propertes of Ada tasg by usg the Ada et laguage are aalyzed ad verfed whch provde a ew ad useful way for aalyzg ad verfyg the complex Ada tasg Key words Ada et sychroous composto sychroous decomposto et laguage aalyss verfcato Receved Jauary ed arch 9 Supported by the Natoal Natural Scece Foudato of Cha uder Grat Nos the Natoal Hgh-ech Research ad Developmet Pla of Cha uder Grat NoAA43 the Natoal Grad Fudametal Research 973 Program of Cha uder Grat NoG the Natoal Scece Foudato for Dstgushed Youg Scholars of Cha uder Grat No 6 the Natoal Research Foudato of the Project for Cadre of Youth eacher of Hgher Educato of Cha the Specal Foudato of Natoal Excellet Doctoral Paper s Wrter uder Grat No99934 the Grad Fudametal Research Foudato of Shagha Scece-echology Developmet Project of Cha uder Grat NoDJ464

《自动化学报》作者加工稿件须知

《自动化学报》作者加工稿件须知智慧科技基于灰色关联度法的智能配电网分级评价 Gradg Evaluato of Itellget Power Dstrbuto Networ Based o Grey Correlato Degree Method 王佳慧赵凤展赵婷婷卫泽晨 2 (. 中国农业大学信息与电气工程学院学院, 北京 00083;2.