http:^^www.cs.utah.edu^projects^formal_verification^
来自「This data set contains WWW-pages collect」· EDU^PROJECTS^FORMAL_VERIFICATION^ 代码 · 共 201 行
EDU^PROJECTS^FORMAL_VERIFICATION^
201 行
Date: Wed, 20 Nov 1996 20:12:34 GMT
Server: Apache/1.1.1+
Content-type: text/html
Content-length: 5354
Last-modified: Wed, 25 Sep 1996 22:37:47 GMT
<! -- $Id: index.html,v 1.4 1996/07/02 17:03:23 ldl Exp ganesh $ --> <HTML><HEAD><TITLE> Formal Methods in System Design and Verification </title></HEAD><BODY bgcolor="ffffff"><hr><h2>University of Utah<br>Department of Computer Science</h2><HR><H3> The Utah Verifier (UV) Project: Formal Methods in System Design and Verification</H3><hr>The UV Cartoon<!WA0><img src="http://www.cs.utah.edu/projects/formal_verification/uv-cartoon.gif" align=middle> <br><HR><H3>Synopsis</H3><p><h4><blockquote>The process of designing modern digital hardware systems(e.g. multiprocessors) is quite challenging in many ways,especially in terms of correctness problems that must besolved. Projects in this area last several years with largegroup sizes, and constantly face changing requirements,personnel turnover, as well as newly unearthed (and oftenunanticipated) facts. Applying today's verification tools toverify entire systems of this nature requires inordinateamounts of human effort as well as computer resources.<p>Under a DARPA award, the Utah Verifier (UV) project hopesto address and solve some of the problems in making formalverification techniques apply to problems of industrial scale.Our ideas are being developed in the context of real systems projects such as<!WA1><a href=http://www.cs.utah.edu/projects/avalanche> Avalanche </a>.Specific activities to date include efficient explicit enumeration methodsbased on new partial-order reduction methods, and model checking of non-trivialindustrial bus specifications. Specific activities planned includecreation of the following suite of verification tools, explained below.<hr>The UV System Block Diagram<!WA2><img src="http://www.cs.utah.edu/projects/formal_verification/uv-system.gif" align=middle> <br><hr><h4> PV: A Protocol Verifier </h4><p>PV will accept descriptions in an extended subset of thePROtocol ModEling LAnguage (Promela) with key extensions in the area of incorporatingabstract data types and uninterpreted functions.It will employ efficienton-the-fly explicit enumeration algorithms.A unique feature of PV will be its supportfor refining high-level protocol descriptionsthat assume infinitely sized communication buffers tothose that use finite- (and/or shared) buffers.<hr><h4> CV: A Cycle-level Verifier </h4><p>CV will accept descriptionsin an extended subset of Verilog, withkey extensions in the area of incorporatingabstract data types.It will perform implicit enumeration efficiently, usingrecently developed graph representations of logic functionssuch as Multiway Decision Graphs (Corella et. al.).CV will also support many pragmatically motivatedfeatures including a facility to accept test vectors fromPV for cross-validating the PV and CV models.<hr><h4> SV: A Switch-level Verifier </h4><p>SV will feature the use of parametric forms of Boolean expressions investigated by usfor incorporating input constraints intosymbolic simulation vectors.The verification conditions to be established by SVthrough symbolic simulation will be derived from the very same descriptions provided to the CV tool.<hr><h4> DB: A Design-requirements Base </h4><p>DB will be shared by members of the project group.The core of DB will be based on the PVS verificationsystem from SRI. The expressive power of the PVS theory descriptionlanguage will permit design requirements to be captured at a high levelof abstraction, and also permit future extensionsto exploit PVS's full power. It will also permit thestate transition relation in PV and CV to be translatedinto PVS to prove key system properties.DB will also have facilities to translate assertions in itsdesign requirements-base into assertions to be verifiedby the PV (mainly for protocol) and CV(mainly for data-layout and cycle-level details)tools, to ensure consistencybetween the models.A valuable aspect of this organization is that it will permitregression verification runs after design changes.The DB tool will have a hypertext-based API allowing designersto pursue links to various pieces of the specification.<hr><h4> Benchmark Examples </h4><p>Benchmark examples cutting across several hierarchical levels ofabstraction will be released. A key verification benchmark-suite delivered will bea distributed shared memory cache protocol, and its refinement through a hardware realization using an industrial bus and a routing network,the refinement of the bus transactions, the refinement of the busarbitration schemes and flow control, all the way down to the businterface logic. <hr><h4> Further Details </h4><p>Prospective graduate studentsand post-doctoral fellows are encouraged to contact <!WA3><a href="mailto:ganesh@cs.utah.edu">ganesh@cs.utah.edu</a>.See <!WA4><a href="http://www.cs.utah.edu/~ganesh/"> http://www.cs.utah.edu/~ganesh</a>for further details.</blockquote><hr><P><H3>Faculty</H3><p><h4><blockquote><ul><li><!WA5><a href="http://www.cs.utah.edu/~ganesh/">Ganesh Gopalakrishnan</a><p><li><!WA6><a href="http://www.cs.utah.edu/~ald/">Alan Davis</a><p></ul></h4></blockquote><p><br><hr><p><h3>Students</h3><ul><h4><blockquote><li><!WA7><a href="http://www.cs.utah.edu/~ratan/">Ratan Nalumasu</a><p><p><li><!WA8><a href="http://www.cs.utah.edu/~hosabett/">Ravi Hosabettu</a><p></ul></h3></blockquote><hr><center><nobr><!WA9><a href="http://www.cs.utah.edu/projects/formal_verification//"><!WA10><img border=0 src="http://www.cs.utah.edu/projects/icons/dept_cs_button.gif"></a><!WA11><a href="http://www.cs.utah.edu/projects/"><!WA12><img border=0src="http://www.cs.utah.edu/projects/icons/research_cs_button.gif"></a></nobr></center><HR></BODY></HTML>⌨️ 快捷键说明
复制代码Ctrl + C
搜索代码Ctrl + F
全屏模式F11
增大字号Ctrl + =
减小字号Ctrl + -
显示快捷键?