Практическое применение языка Alloy для распознавания тактических ситуаций

Автор: Хельвас А.В., Галицкий А.С.

Журнал: Труды Московского физико-технического института @trudy-mipt

Статья в выпуске: 4 (40) т.10, 2018 года.

Бесплатный доступ

В статье рассматривается подход к обнаружению тактических ситуаций на осно- ве анализа формальных утверждений, формируемых путем обработки потока сообще- ний о событиях и угрозах в формализованном виде в информационной системе ситу- ационного центра. Для анализа используется язык Alloy и аналитическое приложение Alloy Analyzer. Рассмотрен пример анализа типичной ситуации обнаружения паводко- вой угрозы.

Тактическая ситуация

Короткий адрес: https://sciup.org/142220463

IDR: 142220463

Список литературы Практическое применение языка Alloy для распознавания тактических ситуаций

Jackson D. Logic, language and analysis. The MIT Press, 2006. 369 p.
Jackson D. Depandable Software by Design//Scientific American, 2006. V. 294, N 6. P. 69-75.
Akhawe, Devdatta and Barth, Adam and Lam, Peifung E. and Mitchell, John and Song, Dawn. Towards a Formal Foundation of Web Security//Proceedings of the 2010 23rd IEEE Computer Security Foundations Symposium. Edinburgh. 2010. P. 290-304.
D.Jackson and M.Jackson. Separating Concerns in Requirements Analysis: An Example//Rigorous Development of Complex Fault-Tolerant Systems. 2006. P. 210-225.
Andrew Rae, Daniel Jackson, Prasad Ramanan, Jay Flanz and Didier Leyman. Critical Feature Analysis of a Radiotherapy Machine//Reliability Engineering and System Safety. 2004.
Dennis G. TSAFE: Building a trusted computing base for air traffic control software. Master’s thesis. MIT. 2003.
Tadjouddine E.M., Guerin F. Verifying Dominant Strategy Equilibria in Auctions//Multi-Agent Systems and Applications. V. 2007. P. 288-297.
Tahina Ramananandro. Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method//Formal Aspects of Computing. 2008. P. 21-39.
Sanjai Narain. Network Configuration Management via Model Finding//LISA ’05 Proceedings of the 19th conference on Large Installation System Administration Conference. 2005. P. 155-168.
Eunsuk Kang, Daniel Jackson. Formal Modeling and Analysis of a Flash Filesystem in Alloy//Abstract State Machines, B and Z. 2008. P. 294-308.
Svendsen A., Moller-Pedersen B., Haugen O., Endresen J., Carlson E. Formalizing Train Control Language: Automating Analysis Of Train Stations//Computers in Railways XII. 2010. P. 245-256.
Frappier M.//Comparison of Model Checking Tools for Information Systems. 2010.
Gassend B., Dijk M.V., Clarke D., Torlak E., Devadas S., Tuyls P. Controlled Physical Random Functions and Applications//ACM Trans. Inf. Syst. Secur. 2008. P. 245-256.
Mana Taghdiri and Daniel Jackson. A Lightweight Formal Analysis of a Multicast Key Management Scheme//In Proceedings of Formal Techniques of Networked and Distributed Systems -FORTE 2003, LNCS. 2003. P. 240-256.
Dennis G., Yessenov K., Jackson D. Bounded Verification of Voting Software//Verified Software: Theories, Tools, Experiments. 2008. P. 130-145.
Vaziri M. Finding Bugs in Software with a Constraint Solver//PhD thesis. MIT. 2004.
Dennis G. A relational framework for bounded program verification//PhD thesis. MIT. 2009.
Harel D., Kugler H., Pnueli A. Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements, H.-J. Kreowski et al. (Eds.): Formal Methods (Ehrig Festschrift), 2006.
Business Process Model and Notation (BPMN). OMG Specification, 2.0. 2011. http://www.omg.org/spec/BPMN/2.0
Common Alerting Protocol Version 1.2. 2010. OASIS Standard http://docs.oasis-open.org/emergency/cap/v1.2/CAP-v1.2-os.pdf]

Еще

Статья научная