General information
Latest issue

Search papers
Search references

Latest issue
Current issues
Archive issues
What is RSS


Personal entry:
Save password
Forgotten password?

Tr. SPIIRAN, 2013, Issue 26, Pages 349–383 (Mi trspy563)  

This article is cited in 5 scientific papers (total in 5 papers)

Tools of Integrated Technology for Analysis and Verification of Telecom Application Specs

I. S. Anureeva, S. N. Baranovb, D. M. Beloglazova, E. V. Bodina, P. D. Drobintsevc, A. V. Kolchind, V. P. Kotlyarovc, A. A. Letichevskiid, O. A. Letychevskyid, V. A. Nepomnyashchiiae, I. V. Nikiforovc, S. V. Potiyenkod, L. V. Priimac, B. V. Tyutinc

a A. P. Ershov Institute of Informatics Systems Sib. Br. RAS
b St. Petersburg Institute for Informatics and Automation of RAS
c Saint-Petersburg State Polytechnical University
d Glushkov Institute of Cybernetics NAS Ukraine
e Novosibirsk State University

Abstract: The paper describes an integrated approach and respective tools which provide methods and means for analysis and verification for representatives of all four major classes of languages used to describe telecom applications: languages of general purpose executable specifications (SDL), languages for high-level descriptions of complex systems behavior patterns and their interconnections (UCM), special purpose language for verification of telecom applications (interpreting MSC, communicating finite state machines, Dynamic-REAL), and industrial imperative languages (C/C++).
Verification of specifications is complemented with automated construction of test suites, which ensure the specified test coverage rate of source behavioral specifications and are optimal with respect to specified performance criteria. Tests are run in a specialized automated test-run environment either on system models, or on actual system implementations inserted in respective program shells which provide communication of the system under test with the test environment. The test shell allows for automated analysis of the test-run results along with the test-runs as well.

Keywords: asic protocols, verification, key agents, operational semantics, safety logic, telecommunication systems, labelled transition systems, specification language SDL, specification language Dynamic-REAL, verification system SPIN, finite automata systems, coloured Petri nets
Author to whom correspondence should be addressed

Full text: PDF file (1276 kB)
References: PDF file   HTML file
UDC: 004.92+004.94
Received: 25.12.2012

Citation: I. S. Anureev, S. N. Baranov, D. M. Beloglazov, E. V. Bodin, P. D. Drobintsev, A. V. Kolchin, V. P. Kotlyarov, A. A. Letichevskii, O. A. Letychevskyi, V. A. Nepomnyashchii, I. V. Nikiforov, S. V. Potiyenko, L. V. Priima, B. V. Tyutin, “Tools of Integrated Technology for Analysis and Verification of Telecom Application Specs”, Tr. SPIIRAN, 26 (2013), 349–383

Citation in format AMSBIB
\by I.~S.~Anureev, S.~N.~Baranov, D.~M.~Beloglazov, E.~V.~Bodin, P.~D.~Drobintsev, A.~V.~Kolchin, V.~P.~Kotlyarov, A.~A.~Letichevskii, O.~A.~Letychevskyi, V.~A.~Nepomnyashchii, I.~V.~Nikiforov, S.~V.~Potiyenko, L.~V.~Priima, B.~V.~Tyutin
\paper Tools of Integrated Technology for Analysis and Verification of Telecom Application Specs
\jour Tr. SPIIRAN
\yr 2013
\vol 26
\pages 349--383

Linking options:

    SHARE: FaceBook Twitter Livejournal

    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles

    This publication is cited in the following articles:
    1. P. D. Drobintsev, V. P. Kotlyarov, I. V. Nikiforov, A. A. Letichevskii, V. S. Peschanenko, “Podkhod k avtomatizatsii otladki povedencheskikh stsenariev”, Model. i analiz inform. sistem, 21:6 (2014), 44–56  mathnet
    2. S. A. Chernenok, V. A. Nepomnyaschii, “Analiz i verifikatsiya MSC-diagramm raspredelennykh sistem s pomoschyu raskrashennykh setei Petri”, Model. i analiz inform. sistem, 21:6 (2014), 94–106  mathnet
    3. P. D. Drobintsev, V. P. Kotlyarov, I. V. Nikiforov, A. A. Letichevskii, “Inkrementalnyi podkhod k tekhnologii sozdaniya testov dlya industrialnykh proektov”, Model. i analiz inform. sistem, 21:6 (2014), 144–154  mathnet
    4. N. V. Vizovitin, V. A. Nepomnyaschii, A. A. Stenenko, “Primenenie raskrashennykh setei Petri dlya verifikatsii konstruktsii upravleniya stsenariyami yazyka UCM”, Model. i analiz inform. sistem, 23:6 (2016), 688–702  mathnet  crossref  mathscinet  elib
    5. P. D. Drobintsev, V. P. Kotlyarov, I. V. Nikiforov, N. V. Voinov, I. A. Selin, “Conversion of abstract behavioral scenarios into scenarios applicable for testing”, Trudy ISP RAN, 28:3 (2016), 145–160  mathnet  crossref  elib
  • Number of views:
    This page:195
    Full text:52
    First page:1

    Contact us:
     Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2020