---
abstract: 'A non-exhaustive collection of files on NuSMV experiments on the mode synchronization protocol in DSAOCSS. The "input files" are mpbase.smv, split.sh, _split.sh, batch.sh, and inc.txt.The file btc.txt and and all lmp??.txt files have been produced by batch.sh that in turn needs mp??.smv files produced by split.sh.The mp??.smv files are not included in this archive because they are easily reproducible and because every mp??.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.'
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id: []
creators_name:
  - family: Varpaaniemi
    given: Kimmo
    honourific: ''
    lineage: ''
data_type: ~
date: 2012-01-10
date_type: completed
datestamp: 2012-01-10 11:33:53
department: ~
dir: disk0/00/00/03/62
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 362
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: other;http://deploy-eprints.ecs.soton.ac.uk/362/1/ModeSyncSBMCbyNuSMV.tar.gz
full_text_status: public
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: unpub
issn: ~
item_issues_comment: []
item_issues_count: ~
item_issues_description: []
item_issues_id: []
item_issues_reported_by: []
item_issues_resolved_by: []
item_issues_status: []
item_issues_timestamp: []
item_issues_type: []
keywords: ~
lastmod: 2012-01-16 11:25:30
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: ~
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: ~
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: Space Systems Finland Ltd
refereed: ~
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 33
series: ~
skill_areas: []
source: ~
status_changed: 2012-01-16 11:25:30
subjects:
  - deploy_industrial
  - deploy_industrial_space
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Some NuSMV Experiments on the Mode Synchronization Protocol in DSAOCSS
type: other
userid: 165
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>