Becoming textual: attempting to model XCHAN with CSPm
Contents
1. A DALE A E Performs Accepts e chan_main_out_ piped_through THE_IMPLEMENTATION P_TESTER y l i P_SERVER l 1 P_ACHAN P CONSUMER gt Allowed Show FDR2 debugger xk FDR Accepts 2 Accepts Observed chan_main out_ piped through Permitted chan _main_in Dismiss In this case it is a failure of liveness which you can tell by the right hand area having the heading Accepts Such a behaviour consists of a perfectly acceptable trace of events performed by THE_IMPLEMENTATION_ OUTER and an unacceptably small set of events that THE_IMPLEMENTATION_ OUTER may then offer to its environment FDR2 manual p27 rewritten for this system x FDR Debug 2 Example 1 E HE_IMPLEMENTATION_OUTER Refuses l 1 chan_main_in_ chan_main_out_ newest_after_overflow THE_IMPLEMENTATION P_TESTER l 1 P_SERVER i 1 d l P Allowed P_ ACHAN P CONSUMER Show W Show tau Acc Ref FDR2 debugger FDR Debug 2 Example 1 a _ i THE_IMPLEMENTATION_OUTER A Performs chan_main_in_ xmessage chan_main_in_ xmessage i 1 THE_IMPLEMENTATIO N P ES ER A i 1 P_SERVER LE P_XCHAN P_CONSUMER W Show tau FDR2 debugger 90 ProBE X Exploring THE_IMPLEMENTATION OUTER File Edit Search Trace a THE _ IMPLEMENT A amp A TION OUTER echan_main_in_ x2. Y A message shall never be lost in XCHAN if there is an available receiver on a message per message basis V Over time a fast producer and slow consumer may cause messages to become lost The XCHAN sending side application layer like P_SERVER is in full control to take whatever action it wants to ensure that the required safety level is upheld Liveness F e Whenever a car or a train approaches the crossing they should eventually be able to cross 10 e XCHAN V lf buffer capacity is reached and no more data arrives all data will eventually be available for a recelver The CSPm requirement and model should then reflect this e We cant just write anything and then press any button to verify that a requested property holds like for any other sw program e However FDR2 or I will pick from its chest of tools whenever have written some CSPm and oress the check button e will then have the determinism property of the good or bad model have written verified e Remember that STOP satisfies any safety specification like a trian that stands still and that STOP is the simplest deadlocked process e Therefore we use several properties to tick off as verified the required properties This sum of the results proves the final system OUTER Ax FDR 2 94 Academic teaching and research release File Assert Process Options Interrupt Help Refinement Specification Model Implementation g gt THE
3. chan_ disturb Figure 2 26 SYNCHRONISES THE SENDER AND RECEIVER END OF AN XCHANNEL BY EXPOSING THE INNER STATE CHANGES TO THE PARTIES P XCHAN xchan ready ready sender has xmessage gt xchan_ Lleg2 commit discard xmessage xmessage gt xchan ready ready send now gt xchan_leg1_ piped_through xmessage gt NN xchan_legZ_ piped_through ighyxmessage gt gt erie xmessage xchan_legl_ newest_after overflowlxmessage gt P_XCHAN pee tee hee eA ae Se ee eee ee a ee ee ee en ee ee R R xchan_ready chan_next P ER xchan_leg1 P_XCHAN xchan_leg2 AAAA chan_right chan _ disturb P_SERVER chan_left Figure 2 P SERVER let P SERVER 5 this num received this wait for receiver this do output this xmessage tag this xmessage this num received none and not this wait for receiver and not this do output xchan ready ready sender has xmessage gt P SERVER 5 this num received true this do output this xmessage tag this xmessage ALWAYS INPUTS MESSAGES AND TRIES this _walt_for_recelver amp xchan_ready_ ready send_now gt TO OUTPUT THEM ON P SERVER 5 this num received false true this xmessage tag this xmessage THE XCHANNEL AND this do output xchan legl this xmessage tag this xmessage gt HANDLES OVERFLOW AT P SERVER 5 none false false null xmessage P SERVER APPLICATION 7 chan left xmessage gt
4. Refuses xchan_leg1_ newest_after_overflow A e e e e rrr rrr e e e e e e e l Refuses xchan_leg1_ piped_ through i N t h a h A refuses xchan_ready_ but P_XCHAN refuses ready_send_now l O a O W PO a O E re n lt Accepts xchan_ready_ ready_sender_has_message j i i Refuses xchan_leg2_ i l A Y l 58 SENDS AND RECEIVES MESSAGES TO FROM THE_IMPLEMENTATION AND TRIES TO SORT OUT OVERFLOW OR NOT P P_SER chan_ left P TESTER 2 chan main in xmessage gt Something in chan next next out gt Open chan left xmessage gt Something out Swapping these here and below causes Assert 11 and 12 to fail Good chan right piped through xmessage gt chan main out piped through xmessage gt P TESTER 2 chan right newest after overflow xmessage gt chan main out newest after overflow xmessage gt P TESTER 2 chan left xmessage gt First after something in chan left xmessage gt Overflow chan left xmessage gt Overflow chan next next out gt Open chan right newest after overflow xmessage gt chan main out newest after overflow xmessage gt P TESTER 2 chan right piped through xmessage gt chan main out piped through xmessage gt P TESTER 2 chan disturb disturb gt P TESTER 2 chan_main_out_ P_TESTER chan_main_in c
5. a test program instead of a specification A test program that sends data and analyses the output to see If they are correct Is not a specification e A specification describes what the implemenation must do in a more general way it Is not a test program 17 Repeated CSPm back to square one Repeated CSPm back to square one Problems 1 Writing a specification that as a consequence of a fast producer and slow consumer will Sooner or later lose data CSPm has no concept of time nor any delay cannot say something like during a burst chan_left must accept one input every tick but chan_right only accepts one output on every sth tick If so a buffer of 5 would store for 5 6 ticks without overflow don t Know which buttons to press in CSPm to specify anything like this And is there another way to say the same Still have not resolved what delayed choice and untimed timeout can do for me They are really undocumented Timed CSP 9 or PAT 11 could perhaps be used for needs like this 2 Writing a specification that would normally pipe all data through but may alternatively lose all data e CSPm has no prioritised choice that would make it possible for me to check chan_ready first if there was nothing there then chan_left would be included in the choice 3 But will my final result here show that for an XCHAN system won t need any of the above Solutions dreamt up more and more
6. difficult solutions Like e trying to simulate prioritised choice by feedback e though had simulated this in one end of the model but then on the other end failed e It became unmanagable for me That s when square one was good to have 21 Repeated CSPm but not back to MM 1 e Realising what CSPm offers and does not offer is in the learning e Only recently in this process ProBE appeared and it made me see and then understand more e Learing to reason about a subpart of the system and see that It is enough that this part Is asserted true in a verification is enough e Starting to discover the Lego bricks and their roles refinement failures failure divergence traces deadlock livelock and determinism Hiding and renaming e Starting to see the basics of CSPm slowly takes me by the hand and leads me to a next level 22 The model s architecture get SSS SSSA SSS a a xchan_ready P_SERVER xchan SS Eee chan_ left Schedu ler Figure 1 P_CONSUMER chan_ disturb chan_next chan_right 23 a ee ee ae ee eee a ee ee ee ee eh xchan_ready P SERVER P XCHAN chan_left xchan_leg1 Figure 2 xchan_leg2 P_CONSUMER chan_ disturb chan_next chan_right datatype datatype datatype datatype datatype datatype channel channel channel channel channel channel channel channel channel channel a e E ee ee eee eee ee ee chan_left Prot Mes
7. for sub processes as well as the root processes This is the same as expanding the specified number of levels of the tree in the FDR debugger noting down the traces for each sub process The BEGIN TRACE END TRACE lines carry additional information indicating the path through from the root to the sub process which generate the particular trace 6 A typical use of depth is when the CSP script uses hiding and compression and extracting the full counter example requires tunneling inside those sub processes This is often the case when the CSP has been automatically generated from some other notation FDR2 produces 6 trails for me have named them Trail 1 to Trail 6 5 6 not listed here space BEGIN batch depth 5 Checking THE_IMPLEMENTATION_OUTER deterministic Starting timer otarting compilation Starting Compiling Reading Loading done Took 0 0 0 seconds Starting timer About to start determinism check Allocated a total of 2 pages of size 128K Compaction produced O chunks of 16K Refinement check Trace error after 2 states Refine checked 2 states With 1 transitions Found 1 example Took 0 0 0 seconds Refinement check Refusal error after 16 states Refine checked 16 states With 16 transitions Allocated a total of 8 pages of size 128K Compaction produced O chunks of 16K xfalse BEGIN BEHAVIOUR example 0 process 0 path 0 BEGIN TRACE Trail 1 chan_main_in_ xmessage
8. going from an English word description specification and trying to model it in CSPm and verifying the model with FDR2 and ProBE Is relevant to this lecture XCHAN was my case that easily motivated me After having learned from my struggling here try to find your own case or try to model XCHAN simpler and better then mail me a ee gt i T ee p See ee e acs A a dl A EAS y zy gt A ot at ESA E pe s Notes on a ial New Channel Pe TELL we mz 15 qa o Ea m o m n xoa TH E _ is aNG _ EG a rr e Te lt a z 12 XCHAN 2 Not modeled here Modeled here XCHAN xchan_data am CCC es gt BUFFERED XCHAN re ee ee ee ee ee ee ee eh NON BUFFERED XCHAN 13 XCHAN 2 Not modeled here NON BUFFERED XCHAN Modeling XCHAN Prof Peter Welch made several models of buffered and unbuffered XCHAN in occam pi during proof reading of the original XCHAN paper 5 have photos of the listings he showed me at CPA 2012 but here is a summary 1 An occam process model of a buffered XCHAN including a modified standard ring buffer xchan occ 2 Anoccam process model of an unbuffered XCHAN Two versions a Uses non implemented extended output and input 2 tho phase write b Uses two explicit readings on XCHAN end first to exit ALT second to pick data In my paper had done reasoning to show The model was presented at th
9. 1 to get it deterministic remove hiding here 3 3 Hiding makes things less obvious and opens for surprises so determinism may fail because of this xk FDR 2 94 Academic teaching and research release File Assert Process Options Refinement Deadlock Livelock Determinism Evaluate Refinement Specification Model g gt THE_SPECIFICATION y check Add eo THE_IMPLEMENTATION deadlock free FD eo THE_IMPLEMENTATION livelock free eo THE_IMPLEMENTATION deterministic FD THE SPECIFICATION T THE_IMPLEMENTATION gt THE SPECIFICATION F THE_IMPLEMENTATION gt THE_SPECIFICATION FD THE_IMPLEMENTATION eo THE_IMPLEMENTATON_OUTER deadlock free FDI Revivals divergence La a ae a a a a a A SR O O O E E E A A am 2 Se THE_SPECIFICATION_OUTER F THE_IMPLEMENTATION_OUTER Me THE_SPECIFICATION_OUTER FD THE_IMPLEMENTATION_OUTER gt CHAOS P_ CONSUMER P_ SERVER P_SPECIFICATION P_SPECIFICATION_BUFF P_TESTER P_XCHAN THE_IMPLEMENTATION THE_IMPLEMENTATION_OUTER THE_SPECIFICATION THE_SPECIFICATION_OUTER WAIT Interrupt Help Implementation g gt THE_IMPLEMENTATI y Clear ul Loading Users teig Documents Dokumenter Autronica NTNU fag XCHAN 201 3 03 20 001 csp 94 FDR2 in baten mode Ira FDR2 batch trace depth 5 refusals Users teig Documents Dokumenter Autronica NTNU fag XCHAN 2013 03 20 001 csp If trace has been selected then report traces
10. Becoming textual attempting to model XCHAN with CSPm OBO Using FDR2 and ProBE tools when state ing Is not enough Refinement Deadlock Livelock Determinism Evaluate P_XCHAN xchan_ready_ ready sender_has_xmessage gt xchan_leg2_ commit_discard xmessage xmessage gt xchan_ready_ ready _send_now gt a a a a 3 yvind Teig Autronica Fire and Security cman Taek pled tee eee P_XCHAN xchan_legl_ newest_after_overflow xmessage gt http www teigfam net o VI nd home xchan_leg2_ newest_after_overflow xmessage gt P XCHAN Lecture material at htto www teigfam net oyvind home technology 063 lecture ntnu Exam lecture for TTK3 Sanntidsteori Real time theory 1 in the spirit of TK8112 The Theory of Concurrency in Real Time Systems 2 Trondheim 15 April 2013 Electrical Engineering D240 12 15 14 00 gt Rev2 after exam same date typos fixed and new layout on References page Rev3 August 2013 the two pages of Modeling XCHAN have been updated LI Introduction 1 Introduction 2 Theory XCHAN 3 Hands on deadlock 4 Determinism analysis of the XCHAN model 5 Conclusion Meeting the requirements e What s a requirement and what is an implementation e How do we know that an implementation fulfills a requirement CSPm also called CSP e CSPm 3 4 is a scripting language that combines CSP process algebra with an expression lan
11. DR2 In batch mode with depth parameter Conclusion 1 Introduction 2 Theory XCHAN 3 Hands on deadlock 4 Determinism analysis of the XCHAN model 5 Conclusion 67 Conclusions 1 CSPm as CSP has a steep learning curve 1K8112 covers the foundations of CSP but CSPm seemed to me to be a more different game than had envisaged 2 How to succeed with FDR2 installation was not so obvious FDR2 on OSX needed X11 XQuartz ProBE runs on WineApp app on OSX Wrote blog note see 5 3 After having become somewhat familiar with FDR2 and ProBE encountered to understand how or if could specify and model XCHAN 8 4 The present model took me quite far with an occam in CSPm approach feel reasonably assured that have specified and implemented models of the real XCHAN But this is in some respects the hardest bit dragging onself from the marsh to solid ground 9 Of course have only scratched the surface of CSP and CSPm 6 It takes time to understand the CSPm landscape even if CSPm is a language to formally treat something as simple as state machines or labeled transition diagrams 68 For NINU 1 recommend the next curriculum to include exercises in CSPm The FDR2 CSPm User Manual 6 is packed with a very interesting language have shown a flavour of it here Because have all minus a flavour left to learn 2 And also doing exercises in PAT the Process Analysis Toolkit from the univer
12. LEVEL if this num received none then P SERVER 5 one this wait for receiver this do output piped through xmessage else P SERVER 5 several this wait for receiver this do output newest after overflow xmessage within P SERVER 5 none false false null xmessage xchan_ready mE E E EE ee Sea ee 1 ME a chan_next P_SERVER P_CONSUMER xchan_leg2 chan_right P_XCHAN chan_left xchan_leg1 chan_ disturb Figure 2 28 P SERVER Let P SERVER 5 this num received this wait for receiver this do output this xmessage tag this xmessage this num received none and not this wait for receiver and not this do output xchan ready Y ready sender has xmessage gt P SERVER 5 this num received true this do output this xmessage tag this xmessage ALWAYS INPUTS r MESSAGES AND TRIES this_wait_for_receiver amp xchan ready ready send now gt TO OUTPUT THEM ON P SERVER 5 this num received false true this xmessage tag this xmessage THE XCHANNEL AND this do output amp xchan legl_ this xmessage tag this xmessage gt HANDLES OVERFLOW AT P SERVER 5 none false false null xmessage P SERVER APPLICATION a 7 chan left xmessage gt LEVEL if this num received none then P SERVER 5 one this wait for receiver this do output piped through xmessage else P SERVER 5 several this wait for receiver this do output newest
13. R FOR EVERY INPUT MAY SEND OUT A TAGGED OUTPUT MESSAGE chan_main_in chan_main_out chan_main_in chan_main_out Figure 5 THE SPECIFICATION OUTER chan main 1n_ xmessage gt No output 1f not anything in and never more outs than ins chan main out piped through xmessage gt THE SPECIFICATION OUTER gt chan_maln_out_ newest _after_overflow xmessage gt THE SPECIFICATION OUTER gt SPECIFIES THE_IMPLEMENTATION OUTER THAT THE_SPECIFICATLON_OUTER FOR EVERY INPUT MAY SEND OUT A TAGGED OUTPUT MESSAGE What value if any does such a general specification have THE SPECIFICATION OUTER chan main 1n_ xmessage gt No output 1f not anything in and never more outs than ins chan main out piped through xmessage gt THE SPECIFICATION OUTER gt chan_maln_out_ newest _after_overflow xmessage gt THE SPECIFICATION OUTER SPECIFIES THE_IMPLEMENTATION_OUTER THAT THE_SPECIFICATLON_ OUTER FOR EVERY INPUT MAY SEND OUT A TAGGED OUTPUT MESSAGE Different from LIL assertions an assertion for refinement compares the whole benaviors of a given process with another orocess e g whether there is a subset relationship 11 Hands on deadlock 1 Introduction 2 Theory XCHAN 3 Hands on deadlock 4 Determinism analysis of the XCHAN model 5 Conclusion 39 Refusals and acceptances Refusals What events a state may not engage in Acceptances What events
14. SX as does the folding editor WinF Again see the blog note 5 e Proved to be as promising as had hoped for during my 1 2 moths of FDR only despair Opened up for a lot of aha experiences Self study 1 After this lecture you should be able to 2 Install and run FDR2 and ProBE 3 Do self study of mbuff csp which is covered as a tutorial in the FDR2 User Manual 6 See 1 4 Specification Example 1 4 1 Multiplexed buffer example and 3 2 2 Getting started started with this but will not go throught it here 4 Continue with other files in the demo directory assume they have been carefully selected to take the student through most of the secret paths Many of these have also been described in the lecture book 12 Roscoe Theory XCHAN 1 Introduction 2 Theory XCHAN 3 Hands on deadlock 4 Determinism analysis of the XCHAN model 5 Conclusion XCHAN 1 XCHANSs Notes on a New Channel Type in Communicating Process Architectures 2012 See 8 10 Why XCHAN here XCHAN by itself is not relevant to this lecture However going from an English word description specification and trying to model it in CSPm and verifying the model with FDR2 and ProBE Is relevant to this lecture XCHAN was my case that easily motivated me A ter having learned from my struggling here try to find your own case 11 Why XCHAN here XCHAN by itself is not relevant to this lecture However
15. _IMPLEMENTATION_OUTER THE_SPECIFICATION_ OUTER FD THE_IMPLEMENTATION_OUTER SETS THE IMPLEMENTATION OUTER THE IMPLEMENTATION chan_left_ chan_right_ chan_next_ chan _disturb_ P TESTER 2 a chan_left_ chan_right_ chan_next_ chan_disturb_ CHAOS P_ CONSUMER P_SERVER THE_IMPLEMENTATION P SPECIFICATION P SPECIFICATION BUFF chan left_ chan_right_ chan _next_ chan disturb_ ares P_TESTER_23 Not deterministic 1f P_TESTER_1 P XCHAN THE_IMPLEMENTATION THE_ IMPLEMENTATION OUTER THE IMPLEMENTATION OUTER NO HIDING THE SPECIFICATION THE_SPECIFICATION OUTER WAIT THE_IMPLEMENTATION_OUTER_NO HIDING ra eo ws Zeman naa A H Loading Users teig Documents Dokumenter Autronica NTNU fag XCHAN 2013 03 25 001 csp 63 Conclusion of non determinism evaluation e After much effort finally found a way to see that my implementation is deterministic From ProBE It also seems to do wnat have told It to do Even if know that nondeterminism comes from hiding had to tune and go all the way described in this section e Observe that have used external choice in all implementations and I Internal or nondeterministic choice only in the specifications FDR 2 94 Academic teaching and research release File Assert Process Options Refinement Deadlock Livelock Determinism Evaluate Interrupt Help CHAOS WAIT e See
16. _SPECIFICATION y Failures divergence g gt THE_IMPLEMENTATIC y Check Add Clear eo THE_IMPLEMENTATION deadlock free FD e THE_IMPLEMENTATION livelock free Me THE_IMPLEMENTATION deterministic FD We THE_SPECIFICATION T THE_IMPLEMENTATION We THE_SPECIFICATION F THE_IMPLEMENTATION assert 6 We THE_SPECIFICATION FD THE_IMPLEMENTATION e THE_IMPLEMENTATION_OUTER deadlock free FD eo THE_IMPLEMENTATION_OUTER livelock free gt THE_IMPLEMENTATION OUTER deterministic FD ef THE_SPECIFICA TION_OUTER M THE_IMPLEMENTATION OUTER THE_SPECIFICATION OUTER F THE_IMPLEMENTATION_OUTER THE_SPECIFICATION OUTER FD THE_IMPLEMENTATION_OUTEF gt CHAOS 3 i P_CONSUMER P_SERVER P SPECIFICATION P SPECIFICATION BUFF P TESTER P XCHAN THE_IMPLEMENTATION THE_ IMPLEMENTATION OUTER THE SPECIFICATION THE SPECIFICATION OUTER WAIT O Loading Users teig Documents Dokumenter Autronica NTNU Fag XCHAN 2013 03 20 001 csp z 48 Understanding X THE IMPLEMENTATION OUTER deterministic F assert THE IMPLEMENTATION assert THE IMPLEMENTATION livelock free assert THE IMPLEMENTATION deterministic assert THE SPECIFICATION T THE IMPLEMENTATION assert THE SPECIFICATION F THE IMPLEMENTATION assert THE SPECIFICATION FD THE IMPLEMENTATION deadlock free assert THE IMPLEMENTATION OUTER deadlock free assert THE IMPLEMENTATION OUTER livelock free assert THE IMPLEMENTATION OUTER deterministic ass
17. _tau _tau _tau _ tau _tau _tau _tau _ tau END TRACE BEGIN ACCEPTANCES chan_main_out_ piped_through END ACCEPTANCES BEGIN REFUSALS chan_main_in_ chan_main_out_ newest_after_overflow END REFUSALS END BEHAVIOUR example 0 process 0 path 0 BEGIN BEHAVIOUR example 0 process 0 path 0 O 55 Trail 2 4 5 6 not shown BEGIN TRACE Trail 2 chan_main_in_ xmessage chan_next_ next_out chan_left_ xmessage _tau _tau _tau _tau _tau chan_right_ piped_through xmessage END TRACE BEGIN ACCEPTANCES chan_main_out_ piped_through END ACCEPTANCES BEGIN REFUSALS chan_disturb_ chan_left_ chan_main_in_ chan_main_out_ newest_after_overflow chan_next_ chan_right_ newest_after_overflow chan_right_ piped_through END REFUSALS END BEHAVIOUR example 0 process 0 path 0 O BEGIN BEHAVIOUR example 0 process 0 path 0 0 O BEGIN TRACE Trail 3 chan_next_ next_out chan_left_ xmessage tau _tau _tau _tau _tau chan_right_ piped_through xmessage END TRACE BEGIN ACCEPTANCES chan_disturb_ chan_left_ chan_next_ END ACCEPTANCES BEGIN REFUSALS chan_right_ newest_after_overflow chan_right_ piped_through END REFUSALS END BEHAVIOUR example 0 process 0 path 0 0 O BEGIN BEHAVIOUR example 0 process 0 path 0 0 0 O BEGIN TRACE Trail 4 chan_next_ next_out chan_left_ xmessage xchan_ready_ ready_sender_has_xmessage xchan_leg2_ commit_discard_xmessage xmessage xchan_ready_ ready_send_now xchan_leg1_ pipe
18. a state must engage In f its environment desires Tne one Is the complement of the other In gt Deadlock FDR2 A O O M 2013 03 06 004 no deadlock then deadlock csp datatype data same_data deadlock_data data event channel any data About to start deadlock check A A A A eee P_A any same_data gt same_datal gt f _A Refinement check a P B any same_ data L gt any deadlock_ data io p_B Refusal error after 2 states A Refine checked 2 states THE_IMPLEMENTATION P_A any P_B With 1 transitions y Found 1 example Took 0 0 0 seconds occam deadlocked here because has semantic meaning in FDR2 it s only syntactic sugar for any same data without direction THE_IMPLEMENTATION l 1 roo Accepts lany same_ data Performs any same data P_B w Show tau THE_IMPLEMENTATION Performs any same_ data P_B w Show tau FOR 2 94 Academic teaching and research rele File Assert N Process Options Interrupt E Help Refinement Deadlock Livelock Determinism Evaluate Deadlock Implementation Model g gt THE_IMPLEMENTATIC y Failures Check Add Clear xe THE_IMPLEMENTATION deadlock free F n H Loading Users teig Documents Dokumenter Autronica NTNU Fag lt a Accepts any deadlock_data Perform
19. after overflow xmessage within P_SERVER_5 none false false null xmessage chan_next xchan_leg1 P_XCHAN xchan_leg2 lila chan_right chan_ disturb mE E E EE ee Sea ee 1 ME a Figure 2 29 P CONSUMER let P CONSUMER 3 this num received this next sequence this xmessage this next sequence 0 chan next next out gt P CONSUMER 3 this num received 1 this xmessage this next sequence 1 amp xchan leg2 commit discard xmessage xmessage gt P CONSUMER 3 this num received 2 xmessage this next sequence 2 amp xchan leg2 piped through xmessage gt TAKES INPUT ON P CONSUMER 3 one 3 xmessage THE XCHANNEL 1 this next sequence 2 amp xchan leg2 newest after overflow xmessage gt WHEN IT Is P CONSUMER 3 several 3 xmessage ALLOWED BY HANDSHAKE TO this next sequence 3 and this num received one chan right piped through this xmessage gt P CONSUMER 3 none null GET RID OF IT this next sequence 3 and this num received several amp chan right newest after overflow this xmessage gt P CONSUMER 3 none null 1 chan disturb disturb gt P CONSUMER 3 this num received this next sequence this xmessage within P CONSUMER 3 none 0 null Do o xchan ready chan_ next P_SERVER P ER chan_left ERV xchan_leg1 P_XCHAN xchan_leg2 SAANS chan_right chan _
20. cations books concurrency PDF of the book exists on the Internet Also see http www cs ox ac uk publications books concurrency The Theory and Practice of Concurrency by A W Roscoe Used during NTNU lectures Prentice Hall 1998 See http www cs ox ac uk publications books concurrency PDF of the book exists on the Internet Also see http www cs ox ac uk publications books concurrency NTNU 15 April 2015 70
21. coe Used during NTNU lectures Prentice Hall 1998 See http www cs ox ac uk publications books concurrency PDF of the book exists on the Internet Also see http www cs ox ac uk publications books concurrency XCHANSs Notes on a New Channel Type by yvind Teig in Communicating Process Architectures 2012 CPA 2012 Proceedings of the 34th WoTUG Technical Meeting pages 155 170 P H Welch et al Eds Open Channel Publishing Ltd 2012 ISBN 978 0 9565409 5 9 2012 The authors and Open Channel Publishing Ltd and the authors Read paper and presentation at at http www teigfam net oyvind pub pub_ details html XCHAN Concurrent and Real time Systems the CSP Approach by Steve Schneider 1999 It also treats Timed CSP not supported in FDR2 Model checking concurrent RSL with CSPm and FDR2 by Lizeth Tapia and Chris George May 2008 The United Nations University UNI IIST report No 393 PAT Process Analysis Toolkit An Enhanced Simulator Model Checker and Refinement Checker for Concurrent and Real time Systems This also takes CSP but does not seem to be able to directly import CSPm Made at Singapore University of Technology and Design School of Computer Engineering Nanyang Technological University and School of Computing National University of Singapore Download from http www patroot com The Theory and Practice of Concurrency by A W Roscoe Used during NTNU lectures Prentice Hall 1998 See http www cs ox ac uk publi
22. d_through xmessage xchan_leg2_ piped_through xmessage chan_right_ piped_through xmessage END TRACE BEGIN ACCEPTANCES chan_disturb_ chan_left_ chan_next_ END ACCEPTANCES BEGIN REFUSALS chan_right_ newest_after_overflow chan_right_ piped_through xchan_leg1_ newest_after_overflow xchan_leg1_ piped_through xchan_leg2_ xchan_ready_ END REFUSALS END BEHAVIOUR example 0 process 0 path 0 0 0 0 BEGIN BEHAVIOUR example 0 process 0 path 0 0 0 0 O 96 Traces acceptances and refusals tables TRACE of THE_IMPLEMENTATION_OUTER deterministic chan_main_in_ chan_main_in_ xmessage xmessage tau jchannextnextout han nextnextout ehannextmextout hannextenextiout S tau chanlefxmessage chan_left_xmessage chan left xmessage____ jhanleft message tan Ip echan ready ready sender has message can ready ready sender_has xmessage tau sI echan leg2 pipe through message cam lega pipe through message q A chan_right_ piped_through xmessage chan_right_ piped_through xmessage O E xmessage ACCEPTANCES of THE_IMPLEMENTATION_OUTER deterministic piped through chan_main_out_pipedthrough POS osease jean distro OOOO mtrs oooO fent foam orate foarte foramen III Ce ss Kchan ready ready sender has message REFUSALS of THE_IMPLEMENTATION_OUTER deterministic There is only external choice in use still we have refusals a A O AE AE wanman O O IEA AE chan_main_out newest afier overiow ehan main out newest ater ave
23. disturb Figure 2 30 EXERCISES THE XCHANNEL AND ALSO CONTAINS THE P_XCHAN HANDLING PROCESS fe SSSA SASS ESA ESAS A See o li xchan_ready chan_next P SERVER P CONSUMER chan_left xchan_leg1 P_XCHAN xchan_leg2 chan_right chan_ disturb i l i l chan_next gt pe chan_left P_SPECIFICATION_BUFF chan left 0 0 P SPECIFICATION 0 chan_right mm gt nn pr e mm MMMM a P chan_disturb Figure 3 IS A COMPOSITE PROCESS OF THE_IMPLEMENTATION AND P_TESTER ii eT aa xchan_ready l chan_next P SERVER P_XCHAN P_ CONSUMER chan_left xchan_leg1 xchan_leg2 chan_ disturb Pt mote chan_right chan_main_in chan_main_out Figure 4 ES See SS SS eS SS se P chan_ left SENDS AND RECEIVES MESSAGES TO FROM THE_IMPLEMENTATION AND HIDES MUCH DETAIL TO SIMPLIFY THE_SPECIFICATION OUTER P TESTER 1 chan_main_in_ xmessage gt Something in chan_next_ next_out gt Send into P_CONSUMER chan Left xmessage gt And tell we re able to take a xmessage chan right piped through xmessage gt chan main out piped through xmessage gt P TESTER 1 chan right newest after overflow xmessage gt chan main out newest after overflow xmessage gt P TESTER 1 chan_left_ xmessage gt P TESTER 1 P TESTER throw xmessage chan disturb disturb gt P TESTER 1 chan disturb disturb gt P_TESTER 1 In_ next chan_ disturb FERRER chan_right chan_main_in cha
24. e fringe at CPA 2103 the year after that XCHAN is implementable An occam Model of XCHANs Peter H WELCH a and yvind TEIG b a School of Computing University of Kent UK b Autronica Fire and Security AS Trondheim Norway See http wotug org cpa2013 programme shtml paper63 ASIDE xchan ready first or xchan ready classic All of Peter Welch s senders get xchan ready true when the connection with the recelver was committed After xchan ready true the sender must send and this is the only place to send This algorithm also fully implements the original XCHAN semantics We could call this the preconfirmed solution The original XCHAN paper may start sending any time but if sending fails then the xchan ready is signalled when the connection with the receiver is fully committed So this Classic solution only uses xchan ready to send after an initial failure At CPA 2013 published a paper about feathering which in fact needs classic XCHAN semantics Selective choice feathering with XCHANs Communicating Process Architectures 2013 CPA 2013 See http www teigfam net oyvind pub pub_details htmifFEATHERING Repeated CSPm back to square one e tried to model XCHAN in CSPm as best as could but for a long time failed to understand the landscape e because tried to look for Lego bricks that don t exist continuously had to go back to square one Being new to this even tried to write
25. ed since it in fact does not disturb at all 62 Finally e Removing hiding in THE_IMPLEMENTATION_OUTER made it deterministic e But only with the much more precise P_TESTER_2 which also relates to overflow gt QED P TESTER 2 chan main _i1n_ xmessage gt Something in chan_next_ next_out gt Open chan_left_ xmessage gt Something out chan_right_ piped through xmessage gt chan_main_out_ piped through xmessage gt P TESTER 2 chan_left_ xmessage gt First after something in chan Left _ xmessage gt Overflow chan _Left_ xmessage gt Overflow chan_next_ next_out gt Open chan _right_ newest_after_overflow xmessage gt chan _main_out_ newest_after_overflow xmessage gt P TESTER 2 chan_disturb_ disturb gt P_TESTER_ 2 SENDS AND RECEIVES MESSAGES TO FROM THE_IMPLEMENTATION AND TRIES TO SORT OUT OVERFLOW OR NOT FDR 2 94 Academic teaching and research release File Assert Process Options Interrupt Help Refinement Deadlock Livelock Determinism Evaluate Refinement Specification Model Implementation el 3 Failures divergence el y Check Add Clear THE_IMPLEMENTATION_OUTER deadlock free FD de THE_IMPLEMENTATION_OUTER livelock free THE_IMPLEMENTATION_OUTER_NO_HIDING deterministic FD THE_SPECIFICATION_OUTER T THE_IMPLEMENTATION_OUTER THE_SPECIFICATION_OUTER F THE
26. ed_throL chan_main_in_ message FLIP SERVER Stone true False piped through xmessagel ixchan_leg _ commit_discard xmessage xmessage gt xchan_ ready ready send _now gt xchan_legl_ pipe tau chan_main_in_ xmessage chan_main_in_ message chan_main_in_ lt message Observe that the ProBE diagram above jumps right into THE_IMPLEMENTATION and then into P_SERVER not THE_IMPLEMENTATION_OUTER 51 ProBE Level 2 THE IMPLEMENTATION chan next next out gt chan left xmessage gt chan right piped through xmessage gt chan main out piped through xmessage gt P TESTER chan right newest after overflow xmessage gt chan main out newest after overflow xmessage gt P TESTER chan left xmessage gt P TESTER P TESTER chan disturb disturb gt P TESTER Level 3 P SERVER P XCHAN P CONSUMER 3 none 1 null chan left xmessage gt chan right piped through xmessage gt chan main out piped through xmessage gt P TESTER chan right newest after overflow xmessage gt chan main out newest after overflow xmessage gt P TESTER Level 4 P SERVER 5 one false false piped through xmessage P_XCHAN P CONSUMER 3 none 1 null echan right piped through xmessage gt chan main out piped through xmessage gt P TESTER chan right newest after overflow xmessage gt chan main out newest after overflow xmessage gt P TESTER Level 5 P SERVER 5 one true false piped
27. ert THE SPECIFICATION OUTER T THE IMPLEMENTATION OUTER assert THE SPECIFICATION OUTER F THE IMPLEMENTATION OUTER assert THE SPECIFICATION OUTER FD THE IMPLEMENTATION OUTER Interrupt Help FDR 2 94 Academic teaching and research release File Assert Process Options Refinement Deadlock Livelock Determinism Evaluate Deterministic Implementation Model g gt THE_IMPLEMENTATI y ii 9 eo a eee Check Add Clear E Fa a E Eike PETE Loke IT Pe he MELC NS LL Li LFI we THE_SPECIFICATION_OUTER T THE_IMPLEMENTATION_OUTER ef THE_SPECIFICATION_OUTER F THE_IMPLEMENTATION_OUTER e THE_SPECIFICATION_OUTER FD THE_IMPLEMENTATION_OUTER THE_IMPLEMENTATION_OUTER deterministic F i a a A e m CHAOS P_CONSUMER P_SERVER P_SPECIFICATION P_SPECIFICATION_BUFF Loading Users teig Documents Dokumenter Autronica NTNU fag xCHAN 201 3 03 20 001 csp 01 02 03 04 05 06 07 08 09 10 11 12 ok ok err err err err ok ok err ok ok ok deadlock property FD livelock property deterministic F safety property FDR2 man p33 liveness or deadlock freedom properties livelock freedom property deadlock property FD livelock property deterministic 4 F i safety property FDR2 man p33 liveness or deadlock freedom properties livelock freedom property 49 600 x FDR Debug 2 FDR2 e 1 of 1 o
28. guage to support the idioms of CSP The three operators bind names to values in the functional language part of CSPm There are no explicit assignments but there are Datatype definitions e l are syntactic sugar There is no sending no receiving just synchronizing on an event and optional exchange of data c x gt P x is syntactic sugar for will synchronise on any event c a e cl binding the name x to each a in the subsequent process definition in letter from P A UofOx e Algorithms may be modeled in CSP not executed only shown that they may be executed the terms executable as used in Promela is not used e Not everything in the book 12 Roscoe is implemented in CSPm f ex synchronous parallel Same terms may even have different names See my blog note 5 for a discussion FDR2 e Compiles CSPm scripts ls Formal System s heavy tool e installed it on OSX Mac OS X binaries Again see my blog note 5 e Uses X11 XQuartz on OSX e Presently beta testing a new version at University of Oxford Source UofOx PrOBE e Also compiles CSPm scripts e Is an animator for CSP processes allowing the user to explore the behaviour of models interactively discovered that the download link was dead and when Oxford had been made aware of this the binaries were restored on 1March2013 e downloaded the vintage Win95 version as there was no OSX version Runs under WineApp app on O
29. han_main_out Figure 4 chan_next At this point this yields the same result as with see of the original P_TESTER 99 DIT Ing logs may be a good Idea 2013 03 25 001 batch log depth5 determinismcheck txt vs 2013 03 20 001 batch log depth5 determinismcheck txt 2013 03 25 001 batch log depth5 determinismcheck txt Users teig 2013 03 20 001 batch log depth5 determinismcheck txt Users teic FDR2 batch trace depth 5 refusals Users teig Documents Dokuj s FDR2 batch trace depth 5 refusals Users teia Documents Doku Checking THE_IMPLEMENTATION_OUTER deterministic Checking THE_IMPLEMENTATION_OUTER deterministic Starting timer Starting compilation Starting Compiling Reading Loading done Took 0 0 0 seconds Starting timer About to start determinism check Allocated a total of 2 pages of size 128K Compaction produced Q chunks of 16K Refinement check Trace error after 3 states Refine checked 3 states With 4 transitions Found 1 example Took 0 0 0 seconds Refinement check Refusal error after 22 states Refine checked 22 states With 25 transitions Allocated a total of 8 pages of size 128K Compaction produced Q chunks of 16K xfalse BEGIN BEHAVIOUR example 0 process 0 path BEGIN TRACE chan_main_in_ xmessage _tau _tau _tau _tau status 9 differences Starting timer Starting compilation Starting Compiling Reading Loading done Took 0 0 0 second
30. m to be part of any process set in FDR2 dont know why They do not show up in ProBE gt CHAOS is a CSPm keyword it can always choose to communicate or reject It is the most deterministic divergence free process 7 e WAIT is not in CSPm It simply is a delay operator e Neither is RUN seen in CSP book 12 It UL CHAOS gt is the process that will deterministically detail perform any event 7 Refinement SETTER na ia 94 Model Implementation Ap Clear Specification els check Add THE_IMPLEMENTATION_OUTER deadlock free FD THE_IMPLEMENTATION_ OUTER livelock free THE_IMPLEMENTATION_OQUTER_NO_HIDING deterministic FDI THE_SPECIFICATION_ OUTER T THE_IMPLEMENTATION_OUTER THE_SPECIFICATION_ OUTER F THE_IMPLEMENTATION OUTER THE_SPECIFICATION OUTER FD THE_IMPLEMENTATION_OUTER Failures divergence P_ SPECIFICATION P_SPECIFICATION_BUFF P_TESTER_1 P_TESTER_2 P_XCHAN THE_IMPLEMENTATION THE_IMPLEMENTATION_OUTER THE_IMPLEMENTATION_OUTER_NO_HIDING THE_SPECIFICATION a E ay gt P PEREA ia Loading Users teig Documents Dokumenter Autronica NTNU fag XCHAN 2013 03 25 001 csp 65 Which tool and when e When ok fulfillment of a property e observe tne assumed behaviour with ProBE e remove some hiding to watch internal detalls gt When error e use FDR2 and ProBE together play around with hiding and renaming e run F
31. message LTHE IMPLEMENTATION co J chan_next_Inext_out chan_ left lxmessage chan_right_ piped through lt message chan_main_out_ piped through lt message gt P_TESTER Jchan_right_ new tau P SERVER 0P CHAN P_ CONSUMER 3 none 0 nall A P_ TESTER chan_main_in_ message P SERVER P CHAN JP CONSUMER 3 none 1 nal chan_ left Ixmessage 2 gt chan_ right piped through lt message gt chan_main_out_ piped_through lt message gt P E pr False False piped_ through xmessage P XCHAN JP CONSUMER 3 mnone 1 nal OC chan_right_ piped_through lt message chan_main_out_ E ESE piped through xmessagel isxcchan leg _ conmmit discard xmessage xmessage gt xchan_ready lready send_now xchan_legl_ pipe E pr False piped through xmessage ixchan_ready lreadw send_now gt xchan_legi_ piped_through message xchan_leg2_ piped_l E e IEEE False true piped through xmessagel Jixchan_legl_ piped through xmessage gt xchan_leg _ piped through xmessage gt P_XCH tau EHP SERVER S none False False null xmessagel ixchan_leg _ piped_ through xmessage gt P_ CHAN JP CONSUMER S3 none 2 messac P SERVER Stone False False piped through xmessagel FP CHANT JP CONSUMER P_ TESTER tau HP SERVER Stone true False piped through messaged xchan_leg2_ cormmit_discard_ message xmessage gt xchan_ready ready send_now fxchan_leg1_ pip
32. n_main_out Figure 4 33 SENDS AND RECEIVES MESSAGES TO FROM THE_IMPLEMENTATION AND HIDES MUCH DETAIL TO SIMPLIFY THE_SPECIFICATION_ OUTER P TESTER 1 Something in en s Send into P_CONSUMER gt And tell we re able to take a xmessage t gt chan main out piped throuqh xmessaqge gt P TESTER 1 chan right newest after over Ww xme 2 gt chan main out newest after over Wi XME 2 gt P TESTER 1 P TESTER throw xmessage chan_ left chan disturb disturb gt P TESTER 1 P_TESTER is also called P_LTESTER_1 chan_disturb_ disturb gt P_TESTER_1 In_ next chan_ disturb FERRER chan_right chan_main_in chan_main_out Figure 4 IS A COMPOSITE PROCESS OF THE_IMPLEMENTATION AND P_TESTER RPS ASS SS SS SSS SS Se SS SSS SES SS Se Se eS ee ee ee ee ee eS xchan_ready l chan_next P SERVER P CONSUMER chan_left E xchan_leg1 P_XCHAN xchan_leg2 chan_ disturb P TESTER chan_right chan_main_in chan_main_out chan_main_in chan_main_out Figure 5 35 A SS SSS SS Se SS SSS SES SS Se Se eS ee ee ee ee ee eS xchan_ready THE SPECIFICATION OUTER chan main 1n_ xmessage gt No output 1f not anything in and never more outs than ins chan main out piped through xmessage gt THE SPECIFICATION OUTER gt chan_maln_out_ newest _after_overflow xmessage gt THE SPECIFICATION OUTER SPECIFIES THE_IMPLEMENTATION OUTER THAT THE SPECIFICATION OUTE
33. o wn OOOO IE AE han Tahi newest afer overiow shan Tight piped Ihrough PO an eg menester overtow chan Jegi newest afer overfow chan leg _newest ater_oveion A an et pied trough fechan legt_piped tough han Jeg1 piped through IS EEN 71 E AT a IO EE ss can ready ready send now O y y 3 Dd pe 57 Drawn by hana chan_main_in_ xmessage THE_IMPLEMENTATION_OUTER p FOSS SSS SS SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSESESSESGESGEEEEEEEE 7 Accepts chan_main_out_ piped_through Refuses chan_main_in_ P TESTER chan_left_ xmessage P SERVER chan_next_ next_out xchan_ready ready sender has xmessage xchan_ready ready_send_now i xchan_leg1_ piped_through xmessage chan_right_ piped_through xmessage P_XCHAN xchan_leg2_ commit_discard_xmessage xmessage xchan_leg2_ piped_through xmessage P_CONSUMER e DS i lt Refuses chan_main_out_ newest_after_overflow f i i chan_disturb_ P_TESTER refuses P_CONSUMER accepts cata gers pans aia Tera a renee o a neat pi ee gt i i chan_left_ P_TESTER refuses P_SERVER accepts a ee a a a R l 0 y chan_next_ P_TESTER refuses P CONSUMER accepts y H Por gt Refuses chan_right_ newest_after_overflow ee AAA PP 2 2 AAA AAA i i Refuses chan_right_ piped through E nda dea tic td rca 4
34. ple 8 process 1 path 0 1 END BEHAVIOUR example 0 process 1 path 0 0 1 status 9 differences Actions 61 2013 03 28 001 batch log depth5 determinismcheck txt Users t 2013 03 25 001 batch log depth5 determinismcheck txt Use BEGIN BEHAVIOUR example 0 process 1 path 0 BEGIN TRACE BEGIN TRACE chan_main_in xmessage chan_main_in xmessage tau E chan_main_in_ xmessage chan_main_in_ xmessage END TRACE END TRACE END BEHAVIOUR example 0 process 1 path 0 END BEHAVIOUR example 0 process 1 path 0 BEGIN BEHAVIOUR example 0 process 1 path 0 0 BEGIN BEHAVIOUR example 0 process 1 path 0 0 J BEGIN TRACE BEGIN TRACE chan_main_in_ xmessage 10 chan_main_in_ xmessage Z chan_main_in_ xmessage E ichan_disturb_ disturb END TRACE chan_main_in_ xmessage E ENN REHAVTNIIR avamnla A nrnaracece 1 nath A A FNN TRACE THE IMPLEMENTATION OUTER THE IMPLEMENTATION OUTER THE IMPLEMENTATION THE IMPLEMENTATION chan left chan right chan next chan left chan right chan next chan disturb P TESTER 1 or P TESTER 2 P TESTER 2 or P TESTER 1 chan left chan right chan next chan left chan right chan next chan disturb tried to remove chan_disturb_ but got the exact same result Then also the _tau were gone because chan_disturb_ was hidden in THE_IMPLEMENTATION_OUTER e Same results with both P TESTER 1 and P TESTER 2 e This should indicate that chan_disturb is correctly model
35. s Starting timer About to start determinism check Allocated a total of 2 pages of size 128K Compaction produced Q chunks of 16K Refinement check Trace error after 2 states Refine checked 2 states With 1 transitions Found 1 example Took 0 0 0 seconds Refinement check Refusal error after 16 states Refine checked 16 states With 16 transitions Allocated a total of 8 pages of size 128K Compaction produced Q chunks of 16K xfalse BEGIN BEHAVIOUR example process path BEGIN TRACE chan_main_in_ xmessage _tau _tau _tau _tau Actions 60 But traces only differ on _tau and aisturb_ 2013 03 25 001 batch log depth5 determinismcheck txt vs 2013 03 20 001 batch log depth5 determinismcheck txt 2013 03 25 001 batch log depth5 determinismcheck txt Users teig 2013 03 20 001 batch log depth5 determinismcheck txt Users teit BEGIN BEHAVIOUR example process 1 path BEGIN TRACE chan main in xmessage chan_main_in_ xmessage END TRACE END BEHAVIOUR example 0 process 1 path 0 BEGIN BEHAVIOUR example process 1 path 0 BEGIN TRACE _ chan main _in_ xmessa chan_right_ piped_through END REFUSALS END BEHAVIOUR example 0 process 0 path 0 BEGIN BEHAVIOUR example 0 process 1 path 0 BEGIN TRACE e chan_main_in_ xmessage END TRACE END BEHAVIOUR example 0 process 1 path 0 chan_main_in_ xmessage BEGIN BEHAVIOUR example 0 process 1 path 0 chan_disturb_ disturb BEGIN TRACE chan_main_in_
36. s any same data w Show tau THE_IMPLEMENTATION l 1 Performs any same data P_A w Show tau 41 Deadlock ProBE A O O M 2013 03 06 004 no deadlock then deadlock csp datatype data same_data deadlock_data data event channel any data PA any 1 same data gt any 1 same datal gt x Exploring THE_IMPLEMENTATIO I y lt un 0 pr a 0 0 y y 0 lt un 0 3 i a 0 wm l V gt P_B any same_data L gt any deadlock_data gt P_B AAA any P_B 3 e PL THE_IMPLEMENTATION P_A Efe THE_IMPLEMENTA TION any same data Canylsame data P A lanyideadiock_data gt P BE Exploring P_ A File Edit Search Trace na File Edit Search Trace File Edit Help in any same _data any same data P_A any same_data gt any same_data gt E Rhany deadlock data gt P_B Whany same_data gt P_4 0 paria E any deadlock data P B any same data gt any deadlock data gt P B Hig y any same_ deta Hany same data Hany same data 42 Deadlock ana niding Hiding can introduce divergence and therefore invalidate many failures divergences model specifications In the stable failures model a system P can deadlock if and only if P y can In other words we can hide absolutely all events and move this hiding as far into the process a
37. s possible using tne principles already discussed 6 035 36 Determinism analysis of the XCHAN model 1 Introduction 2 Theory XCHAN 3 Hands on deadlock 4 Determinism analysis of the XCHAN model 5 Conclusion simply because struggled more with this than with anything else 45 Pick one and satisfy but find the right one s 4 3 Choice of Model The hierarchy of models for CSP are useful because they provide differing amount of information about the processes with a corresponding change in the cost of working in that model It is more efficient to perform a check in the simplest model which provides the required detail FDR2 6 manual page 33 Safety Traces refinement Do not know what will happen STOP ed train fine STOP refines all Liveness Failures refinement Deadlock freedom Constrains what it is permitted to Determinism block and perform Complex Livelock freedom Failures divergence refinement Liveness properties After divergence trace then livelock livelock free Safety also here CHAOS Detect livelock and used Deadlock also here actively to make events not visible deadlock free Determinism also here hidden deterministic FDR2 allows the automatic checking of deadlock and livelock freedom as well as general safety and liveness properties 10 In words safety T e There should never be a train and a car on the cross point at the same time 10 e XCHAN
38. sage Prot Message Tag Prot Next Output Prot Ready Prot Disturb Num Received chan main in_ chan main out chan _ left _ chan mid chan_right_ xchan_legl_ xchan_leg2_ xchan_ready_ chan _next_ chan_disturb_ P_SERVER xmessage next out disturb none one several Prot Message Prot Message Tag Prot Message Prot_Message Prot Message Prot Message Tag Prot Message Prot _HMessage Tag Prot_Message Prot Message Tag Prot Message Prot _ Ready Prot Next Output Prot Disturb AAA AAA AAA xchan_ready m E E E mE E P_XCHAN xchan_leg1 Figure 2 ready sender has xmessage ready_send_now xchan_leg2 piped through newest after overflow commit discard xmessage P_CONSUMER chan_ disturb chan_next chan_right 25 SYNCHRONISES THE SENDER AND RECEIVER END OF AN XCHANNEL BY EXPOSING THE INNER STATE CHANGES TO THE PARTIES P XCHAN xchan ready ready sender has xmessage gt xchan_ Lleg2 commit discard xmessage xmessage gt xchan ready _ ready send now gt xchan_Legl piped through xmessage gt xchan_leg2_ piped through xmessage gt P XCHAN xchan Legl newest after overflow xmessage gt xchan_leg2_ newest _ after overflow xmessage gt P_XCHAN pee tee hee eA ae Se ee eee ee a ee ee ee en ee ee e R xchan_ready chan_next P_SERVER P_CONSUMER xchan_leg2 chan_right P_XCHAN chan_left xchan_leg1
39. sities in singapore and Nanyang 10 Its CSP language also contains LTL Linear Temporal Logic and works with C and Microsoft Contracts Generates code but not for this example since synchronous channels 3 also recommend more group work because It s hard to drag oneself by the hair 4 must thank Sverre Hendseth the lecturer for his guidance and positive attitude 9 He certainly gave me the impression that there was not much prior work to draw on concerning CSPm FDR2 and ProBE at NTNU 69 References Becoming textual attempting to model XCHAN with CSPm Using FDR2 and ProBE tools when state ing is not enough yvind Teig Autronica Fire and Security http www teigfam net oyvind home DO SO Lecture material at http www telgfam net oyvind home technology 063 lecture ntnu O a GSeNSs e TTK3 Sanntidsteori NTNU http www itk ntnu no ansatte Hendseth_Sverre sanntidsteori index html TK8112 The Theory of Concurrency in Real Time Systems NTNU http www ntnu edu studies courses TK8112 Formal Systems Europe http www fsel com University of Oxford http www cs ox ac uk projects concurrency tools binaries for academic use FDR2 notes http www teigfam net oyvind home technology 05 fdr2 notes by yvind Teig lt also contains some theory clarifications FDR2 User Manual Download from http www cs ox ac uk projects concurrency tools The Theory and Practice of Concurrency by A W Ros
40. through xmessage xchan leg2 commit discard xmessage xmessage gt xchan ready ready send now gt xchan legl piped through xmessage gt xchan leg2 piped through xmessage gt P XCHAN xchan legl newest after overflow xmessage gt xchan leg2 newest after overflow xmessage gt P_XCHAN P CONSUMER 3 none 1 null X chan right piped through xmessage gt chan main out piped through xmessage gt P TESTER chan right newest after overflow xmessage gt chan main out newest after overflow xmessage gt P TESTER THIS IS level 5 D p t t right newest after overtlow smessage chan main out Inewest after overflow xmessage gt P TESTERA er tay Level 6 P SERVER 5 one true false piped through xmessage xchan ready ready send now gt xchan legl piped through xmessage gt xchan leg2 piped through xmessage gt P XCHAN xchan legl newest after overflow xmessage gt xchan leg2 newest after overflow xmessage gt P XCHAN P CONSUMER 3 none 2 xmessage chan right piped through xmessage gt chan main out piped through xmessage gt P TESTER chan right newest after overflow xmessage gt chan main out newest after overflow xmessage gt P TESTER Level 7 P SERVER 5 one false true piped through xmessage xchan legl piped through xmessage gt xchan leg2 piped through xmessage gt P XCHAN xchan legl newest after overflow xmessage gt xchan leg2 newest after o
41. verflow xmessage gt P XCHAN P CONSUMER 3 none 2 xmessage chan right piped through xmessage gt chan main out piped through xmessage gt P TESTER chan right newest after overflow xmessage gt chan main out newest after overflow xmessage gt P TESTER 92 ProBE ares X Exploring THE_IMPLEMENTATION_OUTER File Edit Search Trace THE_IMPLEMENTATION OUTER Fechan_main_in_ message Ebchan_main_out_ piped through message Pchan main in xmessage BL P_SERVER_5 none False False null xmessage f P_XCHANT JP_CONSUMER_3 none 0 null chan main in xmessage pe So this is not the trace is it But we discuss no determinisn here Hmm 99 Experimenting with niding experiment 1 removing three hidings will make it deterministic but fail others search for experiment 1 in the 2013 03 20 001 csp file It makes both property sets above and below red line equal THE IMPLEMENTATION xchan ready xchan_legl_ xchan_leg2_ experiment 1 to get it deterministic remove hiding here 1 3 THE SPECIFICATION poor P SPECIFICATION BUFF chan_mid_ P SPECIFICATION chan mid_ experiment 1 to get it deterministic remove hiding here 2 3 Generalized parallel interface parallel sharing THE IMPLEMENTATION OUTER chan left chan right _ chan_next_ chan disturb_ experiment
42. xmessage chan_main_in_ xmessage END TRACE chan_main_in_ xmessage END BEHAVIOUR example 0 process 1 path 0 END TRACE END BEHAVIOUR example 0 process 1 path 0 BEGIN BEHAVIOUR example process 1 path 0 BEGIN ALLOWS BEGIN BEHAVIOUR example process 1 path 0 chan_disturb_ disturb BEGIN ALLOWS END ALLOWS END BEHAVIOUR example 0 process 1 path 0 0 END ALLOWS END BEHAVIOUR example 0 process 1 path 0 0 BEGIN BEHAVIOUR example 0 process 1 path 0 0 0 0 BEGIN ALLOWS BEGIN BEHAVIOUR example process 1 path 0 0 0 0 chan_disturb_ disturb BEGIN ALLOWS END ALLOWS END BEHAVIOUR example 08 process 1 path 0 0 0 0 END ALLOWS END BEHAVIOUR example 0 process 1 path 0 0 0 BEGIN BEHAVIOUR example 0 process 1 path 0 0 0 0 0 BEGIN ALLOWS BEGIN BEHAVIOUR example 0 process 1 path 0 0 0 0 BEGIN ALLOWS END ALLOWS END BEHAVIOUR example 0 process 1 path 0 0 0 0 0 END ALLOWS END BEHAVIOUR example 0 process 1 path 0 0 0 0 0 BEGIN BEHAVIOUR example 0 process 1 path 0 0 0 0 1 BEGIN ALLOWS BEGIN BEHAVIOUR example 8 process 1 path 0 0 0 Q 1 chan_disturb_ disturb BEGIN ALLOWS END ALLOWS END BEHAVIOUR example 0 process 1 path 0 0 0 1 END ALLOWS END BEHAVIOUR example 0 process 1 path 0 0 0 1 BEGIN BEHAVIOUR example process 1 path 0 1 BEGIN TRACE BEGIN BEHAVIOUR example 0 process 1 path 0 1 chan_main_in_ xmessage BEGIN TRACE chan_disturb_ disturb chan_main_in_ xmessage chan_main_in_ xmessage chan_main_in_ xmessage END TRACE END TRACE END BEHAVIOUR exam
Download Pdf Manuals
Related Search