?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=Some+NuSMV+Experiments+on+the+Mode+Synchronization+Protocol+in+DSAOCSS&rft.creator=Varpaaniemi%2C+Kimmo&rft.subject=Industrial+Deployment&rft.subject=Space&rft.description=A+non-exhaustive+collection+of+files+on+NuSMV+experiments+on+the+mode+synchronization+protocol+in+DSAOCSS.+The+%22input+files%22+are+mpbase.smv%2C+split.sh%2C+_split.sh%2C+batch.sh%2C+and+inc.txt.The+file+btc.txt+and+and+all+lmp%3F%3F.txt+files+have+been+produced+by+batch.sh+that+in+turn+needs+mp%3F%3F.smv+files+produced+by+split.sh.The+mp%3F%3F.smv+files+are+not+included+in+this+archive+because+they+are+easily+reproducible+and+because+every+mp%3F%3F.smv+is+simply+a+concatenation+of+mpbase.smv+and+a+single+LTLSPEC+line.+The+file+gdbmp22.txt+is+an+output+of+a+debugging+session+and+is+included+in+order+to+support+the+conjecture+that+all+segmentation+fault+messages+in+btc.txt+are+due+to+effective+running+out+of+memory+in+software+where+use+of+memory+is+not+properly+monitored.&rft.publisher=Space+Systems+Finland+Ltd&rft.date=2012-01-10&rft.type=Other&rft.type=NonPeerReviewed&rft.format=other&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F362%2F1%2FModeSyncSBMCbyNuSMV.tar.gz&rft.identifier=++Varpaaniemi%2C+Kimmo++(2012)+Some+NuSMV+Experiments+on+the+Mode+Synchronization+Protocol+in+DSAOCSS.++Space+Systems+Finland+Ltd.++++(Unpublished)++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F362%2F<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>