Compositional Behavior Modeling and Formal Validation of Canal System Operations with Finite State Automata

Simple item page
dc.contributor.authorAustin, Mark
dc.contributor.authorJohnson, John
dc.date.accessioned2011-06-14T12:57:15Z
dc.date.available2011-06-14T12:57:15Z
dc.date.issued2011-06
dc.description.abstractTraditional approaches to the formal analysis of canal system operations focus on performance. However, now that canal system operations are moving toward increased use of automation in their day-to-day operations, there is a strong need for formal analysis of system functionality with respect to correctness of operations. This report describes a compositional approach to the multi-level behavior modeling and formal validation of canal system operations with hierarchies and networks of finite state automata. Models and specifications of behavior are formally designed as labeled transition systems. To avoid the well-known state explosion problem, we develop a new procedure for viewpoint-action-process traceability, thereby allowing parts of a problem not relevant to a specific decision to be removed from consideration. Key features of the methodology are illustrated through development of behavior models and validation procedures for lockset- and system-level concerns in the Panama Canal System.en_US
dc.identifier.urihttp://hdl.handle.net/1903/11399
dc.language.isoen_USen_US
dc.relation.isAvailableAtInstitute for Systems Researchen_us
dc.relation.isAvailableAtDigital Repository at the University of Marylanden_us
dc.relation.isAvailableAtUniversity of Maryland (College Park, MD)en_us
dc.relation.ispartofseriesTR_2011-04;
dc.subjectbehavior modelingen_US
dc.subjectautomataen_US
dc.subjectprocess modelingen_US
dc.subjectcanal systemen_US
dc.titleCompositional Behavior Modeling and Formal Validation of Canal System Operations with Finite State Automataen_US
dc.typeTechnical Reporten_US

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
report1_edited.pdf
Size:
1.05 MB
Format:
Adobe Portable Document Format
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.64 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

Institute for Systems Research Technical Reports