Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


ucin1026494806.pdf (479.27 KB)

ETD Abstract Container

Abstract Header

Type-Safety Obligation Generation in Rosetta

Kamath, Roshan
http://rave.ohiolink.edu/etdc/view?acc_num=ucin1026494806

Abstract Details

2002, MS, University of Cincinnati, Engineering : Computer Engineering.
The essence of systems engineering is the ability to aggregate heterogeneous information into design decision making processes. The Systems Level Design Language (SLDL) community is currently examining solutions to the problems presented by a heterogeneous modeling language.One such modeling language is Rosetta developed under the aegis of the SLDL forum. To facilitate the use of Rosetta within the system level design community, tools like parsers, theorem provers, model checkers etc. are necessary. The main thrust of this work is towards the development and implementation of a type checking algorithm to facilitate semantic checking in the Rosetta parser. In particular, this work focuses on handling scenarios that present incomplete type information during type checking. For a conventional programming language such cases are explicit semantic errors as their sole purpose is code generation - and code generation almost always needs complete type resolution (except for languages that support dynamic typing). However, for modeling languages that use higher levels of abstraction such type details may not always be specified or available. The solution then is to generate Type-Safety Obligations (TSOs) that need to be proven within the context of the specification being parsed if the specification is to be deemed semantically correct. In this thesis we discuss the motivation and the semantic basis of TSOs. We also identify the different cases where TSOs can be generated and the resulting TSO for each such case. To demonstrate the feasibility of the ideas developed, we also present an example specification and the resulting TSOs that are generated by the Rosetta parser.
Perry Alexander (Advisor)
66 p.
Type Safety; Type Checking; Rosetta; Systems Level Design Language (SLDL); Specification Languages; Formal Methods.

Recommended Citations

Citations

  • Kamath, R. (2002). Type-Safety Obligation Generation in Rosetta [Master's thesis, University of Cincinnati]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1026494806

    APA Style (7th edition)

  • Kamath, Roshan. Type-Safety Obligation Generation in Rosetta. 2002. University of Cincinnati, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=ucin1026494806.

    MLA Style (8th edition)

  • Kamath, Roshan. "Type-Safety Obligation Generation in Rosetta." Master's thesis, University of Cincinnati, 2002. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1026494806

    Chicago Manual of Style (17th edition)

ucin1026494806
647
© 2002, all rights reserved.
This open access ETD is published by University of Cincinnati and OhioLINK.