國立虎尾科技大學 |

Combining Type Checking with Model Checking for System Verification.

Record Type:	Language materials, manuscript : Monograph/item
Title/Author:	Combining Type Checking with Model Checking for System Verification./
Author:	Ren, Zhiqiang.
Description:	1 online resource (182 pages)
Notes:	Source: Dissertation Abstracts International, Volume: 79-05(E), Section: B.
Contained By:	Dissertation Abstracts International79-05B(E).
Subject:	Computer science. -
Online resource:	click for full text (PQDT)
ISBN:	9780355489255

Combining Type Checking with Model Checking for System Verification.
Ren, Zhiqiang.

Combining Type Checking with Model Checking for System Verification. - 1 online resource (182 pages)

Source: Dissertation Abstracts International, Volume: 79-05(E), Section: B.

Thesis (Ph.D.)

Includes bibliographical references

Type checking is widely used in mainstream programming languages to detect programming errors at compile time. Model checking is gaining popularity as an automated technique for systematically analyzing behaviors of systems. My research focuses on combining these two software verification techniques synergically into one platform for the creation of correct models for software designs.

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

Mode of access: World Wide Web

ISBN: 9780355489255Subjects--Topical Terms:

573171
Computer science.
Index Terms--Genre/Form:

554714
Electronic books.

Combining Type Checking with Model Checking for System Verification.
LDR:03534ntm a2200373Ki 4500 001 909092
005 20180419121556.5
006 m o u
007 cr mn||||a|a||
008 190606s2017 xx obm 000 0 eng d
020 $a 9780355489255
035 $a (MiAaPQ)AAI10251764
035 $a (MiAaPQ)bu:12598
035 $a AAI10251764
040 $a MiAaPQ $b eng $c MiAaPQ
099 $a TUL $f hyy $c available through World Wide Web
100 1 $a Ren, Zhiqiang. $3 1179646
245 1 0 $a Combining Type Checking with Model Checking for System Verification.
264 0 $c 2017
300 $a 1 online resource (182 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: 79-05(E), Section: B.
500 $a Adviser: Hongwei Xi.
502 $a Thesis (Ph.D.) $c Boston University $d 2017.
504 $a Includes bibliographical references
520 $a Type checking is widely used in mainstream programming languages to detect programming errors at compile time. Model checking is gaining popularity as an automated technique for systematically analyzing behaviors of systems. My research focuses on combining these two software verification techniques synergically into one platform for the creation of correct models for software designs.
520 $a This thesis describes two modeling languages ATS/PML and ATS/Veri that inherit the advanced type system from an existing programming language ATS, in which both dependent types of Dependent ML style and linear types are supported. A detailed discussion is given for the usage of advanced types to detect modeling errors at the stage of model construction. Going further, various modeling primitives with well-designed types are introduced into my modeling languages to facilitate a synergic combination of type checking with model checking.
520 $a The semantics of ATS/PML is designed to be directly rooted in a well-known modeling language PROMELA. Rules for translation from ATS/PML to PROMELA are designed and a compiler is developed accordingly so that the SPIN model checker can be readily employed to perform checking on models constructed in ATS/PML. ATS/Veri is designed to be a modeling language, which allows a programmer to construct models for real-world multi-threaded software applications in the same way as writing a functional program with support for synchronization, communication, and scheduling among threads. Semantics of ATS/Veri is formally defined for the development of corresponding model checkers and a compiler is built to translate ATS/Veri into CSP# and exploit the state-of-the-art verification platform PAT for model checking ATS/Veri models. The correctness of such a transformational approach is illustrated based on the semantics of ATS/Veri and CSP#.
520 $a In summary, the primary contribution of this thesis lies in the creation of a family of modeling languages with highly expressive types for modeling concurrent software systems as well as the related platform supporting verification via model checking. As such, we can combine type checking and model checking synergically to ensure software correctness with high confidence.
533 $a Electronic reproduction. $b Ann Arbor, Mich. : $c ProQuest, $d 2018
538 $a Mode of access: World Wide Web
650 4 $a Computer science. $3 573171
655 7 $a Electronic books. $2 local $3 554714
690 $a 0984
710 2 $a ProQuest Information and Learning Co. $3 1178819
710 2 $a Boston University. $b Computer Science. $3 1179647
773 0 $t Dissertation Abstracts International $g 79-05B(E).
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=10251764 $z click for full text (PQDT)