東華大學圖書館 |

語系: 繁體中文

說明(常見問題)

回圖書館首頁

手機版館藏查詢

登入

回首頁

切換: 標籤 | MARC模式 | ISBD

Verification and Validation of UML a...

Jarraya, Yosr.

FindBook

Google Book

Amazon

博客來

Verification and Validation of UML and SysML Based Systems Engineering Design Models.

紀錄類型:	書目-語言資料,印刷品 : Monograph/item
正題名/作者:	Verification and Validation of UML and SysML Based Systems Engineering Design Models./
作者:	Jarraya, Yosr.
面頁冊數:	218 p.
附註:	Source: Dissertation Abstracts International, Volume: 71-12, Section: B, page: .
Contained By:	Dissertation Abstracts International71-12B.
標題:	Engineering, Computer. -
電子資源:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=NR67341
ISBN:	9780494673416

Verification and Validation of UML and SysML Based Systems Engineering Design Models.
Jarraya, Yosr.

Verification and Validation of UML and SysML Based Systems Engineering Design Models. - 218 p.

Source: Dissertation Abstracts International, Volume: 71-12, Section: B, page: .

Thesis (Ph.D.)--Concordia University (Canada), 2010.

In this thesis, we address the issue of model-based verification and validation of systems engineering design models expressed using UML/SysML. The main objectives are to assess the design from its structural and behavioral perspectives and to enable a qualitative as well as a quantitative appraisal of its conformance with respect to its requirements and a set of desired properties. To this end, we elaborate a heretofore unattempted unified approach composed of three well-established techniques that are model-checking, static analysis, and software engineering metrics. These techniques are synergistically combined so that they yield a comprehensive and enhanced assessment. Furthermore, we propose to extend this approach with performance analysis and probabilistic assessment of SysML activity diagrams. Thus, we devise an algorithm that systematically maps these diagrams into their corresponding probabilistic models encoded using the specification language of the probabilistic symbolic model-checker PRISM. Moreover, we define a first of its kind probabilistic calculus, namely activity calculus, dedicated to capture the essence of SysML activity diagrams and its underlying operational semantics in terms of Markov decision processes. Furthermore, we propose a formal syntax and operational semantics for the input language of PRISM. Finally, we mathematically prove the soundness of our translation algorithm with respect to the devised operational semantics using a simulation preorder defined upon Markov decision processes.

ISBN: 9780494673416Subjects--Topical Terms:

1669061
Engineering, Computer.

Verification and Validation of UML and SysML Based Systems Engineering Design Models.
LDR:02336nam 2200241 4500 001 1395461
005 20110518115257.5
008 130515s2010 ||||||||||||||||| ||eng d
020 $a 9780494673416
035 $a (UMI)AAINR67341
035 $a AAINR67341
040 $a UMI $c UMI
100 1 $a Jarraya, Yosr. $3 1674154
245 1 0 $a Verification and Validation of UML and SysML Based Systems Engineering Design Models.
300 $a 218 p.
500 $a Source: Dissertation Abstracts International, Volume: 71-12, Section: B, page: .
502 $a Thesis (Ph.D.)--Concordia University (Canada), 2010.
520 $a In this thesis, we address the issue of model-based verification and validation of systems engineering design models expressed using UML/SysML. The main objectives are to assess the design from its structural and behavioral perspectives and to enable a qualitative as well as a quantitative appraisal of its conformance with respect to its requirements and a set of desired properties. To this end, we elaborate a heretofore unattempted unified approach composed of three well-established techniques that are model-checking, static analysis, and software engineering metrics. These techniques are synergistically combined so that they yield a comprehensive and enhanced assessment. Furthermore, we propose to extend this approach with performance analysis and probabilistic assessment of SysML activity diagrams. Thus, we devise an algorithm that systematically maps these diagrams into their corresponding probabilistic models encoded using the specification language of the probabilistic symbolic model-checker PRISM. Moreover, we define a first of its kind probabilistic calculus, namely activity calculus, dedicated to capture the essence of SysML activity diagrams and its underlying operational semantics in terms of Markov decision processes. Furthermore, we propose a formal syntax and operational semantics for the input language of PRISM. Finally, we mathematically prove the soundness of our translation algorithm with respect to the devised operational semantics using a simulation preorder defined upon Markov decision processes.
590 $a School code: 0228.
650 4 $a Engineering, Computer. $3 1669061
690 $a 0464
710 2 $a Concordia University (Canada). $3 1018569
773 0 $t Dissertation Abstracts International $g 71-12B.
790 $a 0228
791 $a Ph.D.
792 $a 2010
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=NR67341