Implementation of Natural Language Specifications of Communication Protocols by Executable Specifications
スポンサーリンク
概要
- 論文の詳細を見る
In a previous work, the authors proposed a method of translating natural language specifications of communication protocols into algebraic axioms in the form of logical formulas. However, such logical formulas are too abstract to be compiled into an executable program directly. This paper proposes a method of implementing such logical formulas by executable algebraic specifications called BE programs. The syntax of BE programs resembles the syntax of LOTOS. However, the BE interpreter, which executes a given BE program, has a finite number of registers and unbounded I/O buffers unlike the concept of processes in LOTOS. Since a natural language specification of a communication protocol often assumes that a protocol machine has registers, the BE interpreter is more appropriate for a model of protocol machines than the concept of processes in LOTOS. In this implementation method, the meaning of each predicate appearing in logical formulas and denoting actions of a protocol machine is defined as a BE program and stored as a "lexical item" of the predicate. Then a BE program for the logical formulas is constructed in a bottom-up manner. The whole translation from natural language specifications of communication protocols into executable specifications is simple and concise, since the BE interpreter is appropriate for a model of protocol machines and the whole translation is defined within a single framework of algebraic specification methods.
- 一般社団法人情報処理学会の論文
- 1995-05-15
著者
-
KASAMI Tadao
Graduate School of Information Science, Nara Institute of Science and Technology
-
Kasami Tadao
Graduate School Of Information Science Nara Institute Of Science And Technology
-
Koumoto Takuya
Okayama University
-
Ishihara Y
Osaka Univ. Toyonaka‐shi Jpn
-
Seki H
Graduate School Of Information Science Nara Institute Of Science And Technology
-
ISHIHARA Yasunori
Graduate School of Information Science, Nara Institute of Science and Technology
-
SEKI Hiroyuki
Graduate School of Information Science, Nara Institute of Science and Technology
-
Koumoto T
Hiroshima City Univ. Hiroshima Jpn
-
Ishihara Yasunori
Graduate School Of Information Science And Technology Osaka University
-
Seki Hiroyuki
Graduate School Of Information Science Nara Institute Of Science And Technology
関連論文
- MAP and LogMAP Decoding Algorithms for Linear Block Codes Using a Code Structure(Special Section on Information Theory and Its Applications)
- A Recursive Maximum Likelihood Decoding Algorithm for Some Transitive Invariant Binary Block Codes
- A Sufficient Condition for Ruling Out Some Useless Test Error Patterns in Iterative Decoding Algorithms
- Low Weight Subtrellises for Binary Linear Block Codes and Their Applications
- Error Performance of Multilevel Block Coded 8-PSK Modulations Using Unequal Error Protection Codes for the Rayleigh Fading Channel
- An Improved Union Bound on Block Error Probability for Closest Coset Decoding
- On Branch Labels of Parallel Components of the L-Section Minimal Trellis Diagrams for Binary Linear Block Codes
- On Structural Complexity of the L-Section Minimal Trellis Diagrams for Binary Linear Block Codes (Special Section on Information Theory and Its Applications)
- Structural Analysis of Minimum Weight Codewords of the Extended (32, 21, 6) and (64, 45, 8) BCH Codes Using Invariance Property(HISC2006)
- The structure of the set of minimum weight codewords of the extended (32,21,6) and (64,45,8) BCH codes
- Sufficient Conditions for Ruling-Out Useless Iterative Steps in a Class of Iterative Decoding Algorithms (Special Section on Information Theory and Its Applications)
- The Weight Distributions of Cosets of the Second-Order Reed-Muller Code of Length 128 in the Third-Order Reed-Muller Code of Length 128
- A Method for Computing the Weight Distribution of a Block Code by Using Its Trellis Diagram (Special Section on Information Theory and Its Applications)
- An Improved Method for Formal Security Verification of Cryptographic Protocols
- A System for Deciding the Security of Cryptographic Protocols (Special Section on Cryptography and Information Security)
- Computational Complexity of Finding Highly Co-occurrent Itemsets in Market Basket Databases
- Performance Analysis for Binary Image of Linear Block Codes over an Extended Field of GF(2)
- Adaptive Recursive Maximum Likelihood Decoding Based on the Coarsest Parallel Concatenation Decomposition : Evaluation of the Decoding Complexity by Simulation
- Soft-Input Soft-Output Decoding Algorithm Based on Iterative Minimum Distance Search for Reed-Muller Codes
- Selecting the Search Centers of h-Chase Decoding Algorithms by Simulation
- The Optimal Sectionalized Trellises for the Generalized Version of Viterbi Algorithm of Linear Block Codes and Its Application to Reed-Muller Codes
- Average Complexity Evaluation of an MLD Algorithm Using the Trellis Structure for a Linear Block Code
- Verification of the Security against Inference Attacks on XML Databases
- A Formal Approach to Detecting Security Flaws in Object-Oriented Databases (Special Issue on New Generation Database Technologies)
- An Authorization Model for Object-Oriented Databases and Its Efficient Access Control
- Assignment of Data Types to Words in a Natural Language Specification
- Implementation of Natural Language Specifications of Communication Protocols by Executable Specifications
- A Translation Method from Natural Language Specifications of Communication Protocols into Algebraic Specifications Using Contextual Dependencies
- Complexity of the Type-Consistency Problem for Acyclic Object-Oriented Database Schemas
- RNA Pseudoknotted Structure Prediction Using Stochastic Multiple Context-Free Grammar
- On the Generative Power of Grammars for RNA Secondary Structure(Foundations of Computer Science)
- RIGHT-LINEAR FINITE PATH OVERLAPPING REWRITE SYSTEMS EFFECTIVELY PRESERVE RECOGNIZABILITY
- A Soft-Decision Iterative Decoding Algorithm Using a Top-Down and Recursive Minimum Distance Search(Special Section on Information Theory and Its Applications)
- An Evaluation Method of the Block Error Probability by Using a Low-Weight Sub-Trellis Diagram
- Syntactic Unification Problems under Constrained Substitutions
- A Polynomial Time Learning Algorithm for Recognizable Series
- Layered Transducing Term Rewriting System and Its Recognizability Preserving Property (Special Issue on Selected Papers from LA Symposium)
- Termination Property of Inverse Finite Path Overlapping Term Rewriting System is Decidable
- A Polynomial-Time Recognizable Subclass of Lexical-Functional Grammars
- A Note on Inadequacy of the Model for Learning from Queries
- Finite State Translation Systems and Parallel Multiple Context-Free Grammars
- The Universal Recognition Problems for Multiple Context-Free Grammars and for Linear Context-Free Rewriting Systems
- Selection of Test Patterns in an Iterative Erasure and Error Decoding Algorithm for Non-binary Block Codes(Coding Theory)
- Selection Method of Test Patterns in Soft-Decision Iterative Bounded Distance Decoding Algorithms(Coding Theory)(Information Theory and Its Applications)
- Selection of Search Centers in Iterative Soft-Decision Decoding Algorithms(Special Section on Information Theory and Its Applications)
- An Improvement to GMD-Like Decoding Algorithms(Special Section on Information Theory and Its Applications)
- A Labeled Transition Model A-LTS for History-Based Aspect Weaving and Its Expressive Power
- New certificate chain discovery methods for trust establishment in ad hoc networks and their evaluation (特集:次世代社会基盤をもたらす高度交通システムとモバイル通信システム)
- Policy Controlled System and Its Model Checking
- Decidability of the Security Verification Problem for Programs with Stack Inspection
- Reduced Complexity Iterative Decoding Using a Sub-Optimum Minimum Distance Search(Cording Theory)(Information Theory and Its Applications)
- Tree Automaton with Tree Memory
- Sufficient Conditions for Update Operations on Object-Oriented Database to Preserve the Security against Inference Attacks(Databases)
- Security against Inference Attacks on Negative Information in Object-Oriented Databases(Database)
- Static Analysis for k-secrecy against Inference Attacks
- An Efficient Method for Optimal Probe Deployment of Distributed IDS(Dependable Computing)
- RNA Pseudoknotted Structure Prediction Using Stochastic Multiple Context-Free Grammar
- Deciding Schema k-Secrecy for XML Databases
- A Static Analysis using Tree Automata for XML Access Control
- New Certificate Chain Discovery Methods for Trust Establishment in Ad Hoc Networks and Their Evaluation
- New Certificate Chain Discovery Methods for Trust Establishment in Ad Hoc Networks and Their Evaluation
- Runtime Control of a Program based on Quantitative Information Flow