Intro Background Projects Offers Publications Downloads Staff
ISPRAS Description Logo
Home   R&D Groups   Projects   Grants   Publications   Downloads


MSR IPv6 verification:

      Goal - RFC requirements formalization in the form of formal specifications and testing of IPv6 implementation for conformance to these specifications

  • Customer - Microsoft Research
  • Period - 2001
  • Labor expenditures - 3 man*years
  • Publications
       See the white paper "MSR IPv6 Verification within the CTesK-lite Framework" in

    See the completed research grant "MSRIPv6 Verification Project" in

J@T - Java Testing toolkit:

      Goal - development of tool for specification-based Java API test support with specifications written in specification extension of Java language

  • Customer - Advanced Technical Services APS
  • Period - 2000-2002
  • Labor expenditures - 18 man*years
  • Publications
       A.Petrenko. Specification Based Testing: Towards Practice.- VI Ershov Conference Proc., LNCS 2244, 2001.

    I.B.Burdonov, A.V.Demakov, A.A.Jarov, A.S.Kossatchev, V.V.Kuliamin, A.K.Petrenko, S.V.Zelenov. - J@va : extension of Java for real-life specification and testing.- IV Ershov Conference Proc., LNCS 2244, 2001.

KVEST - Kernel VErification & Specification Technology:

      Goal - productization of specification-based testing technology

  • Customer - Nortel Networks
  • Period - 1994-1998
  • Labor expenditures - 20 man*year
  • Publications

KV - Kernel Verification project:

      Goal - development of formal specifications for operating system kernel API and implementation of test system running conformance testing automatically

  • Customer - Nortel Networks
  • Period - 1994-1996
  • Labor expenditures - 10 man*year
  • Publications
       I.Bourdonov, A.V.Demakov, A.Kossatchev, A.Petrenko, and D.Galter. KVEST: Automated Generation of Test Suites from Formal Specifications. Proceedings of World Congress of Formal Methods, Toulouse, France, LNCS, No. 1708, 1999, pp. 608-621.

Intel grant dated at September 15, 2001:

      Result - a method for testing optimizing blocks of compilers based on abstract models is proposed

      Special features of method:

  • Data models and abstract iterators of intermediate representation are developed
  • Experiments were run to demonstrate the possibility of reaching 60-80% code coverage without the knowledge about specific features of optimizing transformations, that opens up the possibilities to lower the testing costs for such programs

RFBR (Russian Foundation for Basic Research) grants - 96-01-01277, 99-01-00207, 02-01-00959:

      Result - UniTesK methodology for specification-based testing is developed

      UniTesK features:

  • Common scheme for programming languages extension for specification and test design purpose
  • Unified architecture of verification set
  • Implicit final state machines as a base for test sequence generation
  • Inheritance and refinement mechanism for higher reuse of artefacts during specifications and tests development


Copyright © 2002 ISP RAS