View in EDS

Uncertainty Problem in High-level Model Based Trace Analysis as Part of Runtime Verification.

Saved in:
Bibliographic Details
Title: Uncertainty Problem in High-level Model Based Trace Analysis as Part of Runtime Verification.
Authors: Karnov, A.1 (AUTHOR) karnov@ispras.ru
Source: Programming & Computer Software. Dec2025, Vol. 51 Issue 7, p478-485. 8p.
Subjects: Linux operating systems, Security systems, Computer operating systems, System analysis, Mathematical optimization
Abstract: The article discusses the problem of applying runtime verification to large and complex systems such as general-purpose operating systems. When verifying the security mechanisms of operating systems, modern practices and standards require a formal security policy model (SPM). The SPM must be verified using formal model methods, and it must also be used to verify the completeness and consistency of the operating system's security mechanisms by confirming compliance with the formal requirements of the SPM. In this case, it is convenient to have a single model suitable for both formal verification and implementation testing. For practical application, it is necessary, on the one hand, to select a subset of model language constructs suitable for both acts, and on the other hand, to develop special techniques for analyzing execution traces that allow to effectively perform thousands of test cases. The article addresses both of these issues. We present an analysis of language constructs that allow us to use the model for both verification and execution trace analysis. We also offer techniques that have been developed to optimize the runtime verification of Linux-based systems. [ABSTRACT FROM AUTHOR]
Copyright of Programming & Computer Software is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 190958816
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Uncertainty Problem in High-level Model Based Trace Analysis as Part of Runtime Verification.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Karnov%2C+A%2E%22">Karnov, A.</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> karnov@ispras.ru</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Programming+%26+Computer+Software%22">Programming & Computer Software</searchLink>. Dec2025, Vol. 51 Issue 7, p478-485. 8p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Linux+operating+systems%22">Linux operating systems</searchLink><br /><searchLink fieldCode="DE" term="%22Security+systems%22">Security systems</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+operating+systems%22">Computer operating systems</searchLink><br /><searchLink fieldCode="DE" term="%22System+analysis%22">System analysis</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+optimization%22">Mathematical optimization</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: The article discusses the problem of applying runtime verification to large and complex systems such as general-purpose operating systems. When verifying the security mechanisms of operating systems, modern practices and standards require a formal security policy model (SPM). The SPM must be verified using formal model methods, and it must also be used to verify the completeness and consistency of the operating system's security mechanisms by confirming compliance with the formal requirements of the SPM. In this case, it is convenient to have a single model suitable for both formal verification and implementation testing. For practical application, it is necessary, on the one hand, to select a subset of model language constructs suitable for both acts, and on the other hand, to develop special techniques for analyzing execution traces that allow to effectively perform thousands of test cases. The article addresses both of these issues. We present an analysis of language constructs that allow us to use the model for both verification and execution trace analysis. We also offer techniques that have been developed to optimize the runtime verification of Linux-based systems. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Programming & Computer Software is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=190958816
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1134/S0361768825700355
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 8
        StartPage: 478
    Subjects:
      – SubjectFull: Linux operating systems
        Type: general
      – SubjectFull: Security systems
        Type: general
      – SubjectFull: Computer operating systems
        Type: general
      – SubjectFull: System analysis
        Type: general
      – SubjectFull: Mathematical optimization
        Type: general
    Titles:
      – TitleFull: Uncertainty Problem in High-level Model Based Trace Analysis as Part of Runtime Verification.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Karnov, A.
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 15
              M: 12
              Text: Dec2025
              Type: published
              Y: 2025
          Identifiers:
            – Type: issn-print
              Value: 03617688
          Numbering:
            – Type: volume
              Value: 51
            – Type: issue
              Value: 7
          Titles:
            – TitleFull: Programming & Computer Software
              Type: main
ResultId 1