Using SPIN for verification of multiagent data analysis
| Autor: | Elena A. Sidorova, Natalya Olegovna Garanina, E. V. Bodin |
|---|---|
| Rok vydání: | 2015 |
| Předmět: |
Model checking
021110 strategic defence & security studies education.field_of_study Data processing Theoretical computer science Computer science Property (programming) Population 0211 other engineering and technologies 02 engineering and technology Ontology (information science) Promela Control and Systems Engineering Signal Processing 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Tuple education Formal verification computer Software computer.programming_language |
| Zdroj: | Automatic Control and Computer Sciences. 49:420-429 |
| ISSN: | 1558-108X 0146-4116 |
| DOI: | 10.3103/s014641161507007x |
| Popis: | The paper presents an approach to formal verification of multiagent data analysis algorithms for ontology population. The system agents correspond to information items of the input data and the rule of ontology population and data processing. They determine values of information objects obtained at the preliminary phase of the analysis. The agents working in parallel check the syntactic and semantic consistency of tuples of information items. Since the agents operate in parallel, it is necessary to verify some important properties of the system related to it, such as the property that the controller agent correctly determines the system termination. In our approach, the SPIN model checking tool is used. The agent protocols are written in the Promela language (the input language of the tool), and the properties of the multiagent data analysis system are expressed in liner time logic (LTL). We carried out several experiments to check this model in various modes of the tool and for various numbers of agents. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink