國立虎尾科技大學 |

Model-Based Usability Analysis of Safety-Critical Systems : = A Formal Methods Framework.

紀錄類型:	書目-語言資料,手稿 : Monograph/item
正題名/作者:	Model-Based Usability Analysis of Safety-Critical Systems :/
其他題名:	A Formal Methods Framework.
作者:	Abbate, Andrew J.
面頁冊數:	1 online resource (482 pages)
附註:	Source: Dissertation Abstracts International, Volume: 78-11(E), Section: B.
Contained By:	Dissertation Abstracts International78-11B(E).
標題:	Systems science. -
電子資源:	click for full text (PQDT)
ISBN:	9780355039290

Model-Based Usability Analysis of Safety-Critical Systems : = A Formal Methods Framework.
Abbate, Andrew J.

Model-Based Usability Analysis of Safety-Critical Systems :A Formal Methods Framework. - 1 online resource (482 pages)

Source: Dissertation Abstracts International, Volume: 78-11(E), Section: B.

Thesis (Ph.D.)

Includes bibliographical references

Complex, safety-critical systems are designed with a broad range of automated and configurable components, and usability problems often emerge for the end user during setup, operation, and troubleshooting procedures. Usability evaluations should consider the entire human-device interface including displays, controls, hardware configurations, and user documentation/procedures. To support the analyst, human factors researchers have developed a set of methods and measures for evaluating human-system interface usability, while formal methods researchers have developed a set of model-based technologies that enable mathematical verification of desired system behaviors. At the intersection of these disciplines, an evolving set of model-based frameworks enable highly automated verification of usability early in the design cycle. Models can be abstracted to enable broad coverage of possible problems, while measures can be formally verified to "prove" that the system is usable. Currently, frameworks cover a subset of the target system and user behaviors that must be modeled to ensure usability: procedures, visual displays, user controls, automation, and possible interactions among them. Similarly, verification methodologies focus on a subset of potential usability problems with respect to modeled interactions.

Electronic reproduction.
Ann Arbor, Mich. :
ProQuest,
2018

Mode of access: World Wide Web

ISBN: 9780355039290Subjects--Topical Terms:

1148479
Systems science.
Index Terms--Genre/Form:

554714
Electronic books.

Model-Based Usability Analysis of Safety-Critical Systems : = A Formal Methods Framework.
LDR:05389ntm a2200385Ki 4500 001 911531
005 20180529094435.5
006 m o u
007 cr mn||||a|a||
008 190606s2017 xx obm 000 0 eng d
020 $a 9780355039290
035 $a (MiAaPQ)AAI10260664
035 $a (MiAaPQ)drexel:10961
035 $a AAI10260664
040 $a MiAaPQ $b eng $c MiAaPQ
099 $a TUL $f hyy $c available through World Wide Web
100 1 $a Abbate, Andrew J. $3 1183415
245 1 0 $a Model-Based Usability Analysis of Safety-Critical Systems : $b A Formal Methods Framework.
264 0 $c 2017
300 $a 1 online resource (482 pages)
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
500 $a Source: Dissertation Abstracts International, Volume: 78-11(E), Section: B.
500 $a Advisers: Amy L. Throckmorton; Ellen J. Bass.
502 $a Thesis (Ph.D.) $c Drexel University $d 2017.
504 $a Includes bibliographical references
520 $a Complex, safety-critical systems are designed with a broad range of automated and configurable components, and usability problems often emerge for the end user during setup, operation, and troubleshooting procedures. Usability evaluations should consider the entire human-device interface including displays, controls, hardware configurations, and user documentation/procedures. To support the analyst, human factors researchers have developed a set of methods and measures for evaluating human-system interface usability, while formal methods researchers have developed a set of model-based technologies that enable mathematical verification of desired system behaviors. At the intersection of these disciplines, an evolving set of model-based frameworks enable highly automated verification of usability early in the design cycle. Models can be abstracted to enable broad coverage of possible problems, while measures can be formally verified to "prove" that the system is usable. Currently, frameworks cover a subset of the target system and user behaviors that must be modeled to ensure usability: procedures, visual displays, user controls, automation, and possible interactions among them. Similarly, verification methodologies focus on a subset of potential usability problems with respect to modeled interactions.
520 $a This work provides an integrated formal methods framework enabling the holistic modeling and verification of safety-critical system usability. Building toward the framework, a set of five, novel approaches extend the capabilities of extant frameworks in different ways. Each approach is demonstrated in a medical device case study to show how the methods can be employed to identify potential usability problems in existing systems. A formal approach to documentation navigation models an end user navigating through a printed or electronic document and verifies page reachability. A formal approach to procedures in documentation models an end user executing steps as written and aids in identifying problems involving what device components are identified in task descriptions, what system configurations are addressed, and what temporal orderings of procedural steps could be improved. A formal approach to hardware configurability models end-user motor capabilities, relationships among the user and device components in the spatial environment, and opportunities for the user to physically manipulate components. An encoding tool facilitates the modeling process, while a verification methodology aids in ensuring that configurable hardware supports correct end- user actions and prevents incorrect ones. A formal approach to interface understandability models what information is provided to the end user through visual, audible, and haptic sensory channels, including explanations provided in accompanying documentation. An encoding tools facilitates the development of models and specifications, while the verification methodology aids in ensuring that what is displayed on the device is consistent; and, if needed, an explanation of what is displayed is provided in documentation. A formal approach to controlled actuators leverages an existing modeling technique and data collected from other engineering activities to model actuator dynamics mapping to referent data. An encoding tool facilitates model development, and a verification methodology aids in validating the model with respect to source data.
520 $a Finally, new methodologies are combined within the integrated framework. A model architecture supports the analyst in representing a broad range of interactions among constituent framework models, and a set of ten specifications is developed to enable holistic usability verification. An implementation of the framework is demonstrated within a case study based on a medical device under development. This application shows how the framework could be utilized early in the design of a safety-critical system, without the need for a fully implemented device or a team of human evaluators.
533 $a Electronic reproduction. $b Ann Arbor, Mich. : $c ProQuest, $d 2018
538 $a Mode of access: World Wide Web
650 4 $a Systems science. $3 1148479
650 4 $a Engineering. $3 561152
650 4 $a Design. $3 595500
655 7 $a Electronic books. $2 local $3 554714
690 $a 0790
690 $a 0537
690 $a 0389
710 2 $a ProQuest Information and Learning Co. $3 1178819
710 2 $a Drexel University. $b Biomedical Engineering, Science, and Health Systems. $3 1183416
773 0 $t Dissertation Abstracts International $g 78-11B(E).
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=10260664 $z click for full text (PQDT)