Utilizing Event-B for domain engineering: a critical analysis
Tóm tắt
Từ khóa
Tài liệu tham khảo
Specification Case Studies in RAISE. Springer, London, UK (2002)
Abrial JR (2010) Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge
Aziz B, Arenas AE, Bicarregui J, Ponsard C, Massonet P (2009) From goal-oriented requirements to Event-B specifications. In: First Nasa formal method symposium. California, US
Baille G, Garnier P, Mathieu H, Roger PG (1999) Le cycab de l’INRIA rhônes-alpes. Technical Report RT-0229, INRIA—Rhônes-Alpes
Bicarregui J, Arenas A, Aziz B, Massonet P, Ponsard C (2008) Towards modelling obligations in Event-B. In: Proceedings of the 1st international conference on Abstract State Machines, B and Z, ABZ ’08. Springer, New York, pp 181–194
Bisztray D, Heckel R, Ehrig H (2008) Verification of architectural refactorings by rule extraction. In: FASE’08/ETAPS’08: proceedings of the Theory and practice of software, 11th international conference on Fundamental approaches to software engineering. Springer, Berlin, pp 347–361
Bjørner D (2006) Software engineering 3: domains, requirements, and software design (texts in theoretical computer science, an EATCS series). Springer, New York
Bjørner D (2007) Development of transportation systems. In: International symposium on leveraging applications of formal methods, Verification and Validation (ISOLA)
Bjørner D (2009) DOMAIN ENGINEERING: technology management, research and engineering. JAIST, Japan
Butler M (2002) A system-based approach to the formal development of embedded controllers for a railway. Des Autom Embed Syst 6:355–366
Butler M (2009) Decomposition structures for Event-B. In: Proceedings of the 7th international conference on integrated formal methods, IFM ’09. Springer, Berlin, pp 20–38
Cansell D, Mery D, Rehm J (2007) Time constraint patterns for event B development. In: Julliand J, Kouchnarenko O (eds) 7th International conference of B users, LNCS, vol 4355. Springer, New York, pp 140–154
Clearsy (2009) User manual of Atelier B, version 4.0
Czarnecki K, Eisenecker UW (2000) Generative programming: methods, tools, and applications. ACM Press/Addison-Wesley Publishing Co., New York
Erasmy F, Sekerinski E (1995) Raise: a rigorous approach using stepwise refinement. In: Lewerentz C, Lindner T (eds) Formal development of reactive systems. Lecture Notes in Computer Science, vol 891. Springer, Berlin, pp 277–293
Essamé D (2004) Handling safety critical requirements in system engineering using the b formal method. In: Heisel M, Liggesmeyer P, Wittmann S (eds) Computer safety, reliability, and security. Lecture Notes in Computer Science, vol 3219. Springer, Berlin, p 115
Futatsugi K, Goguen JA, Jouannaud JP, Meseguer J (1985) Principles of obj2. In: POPL ’85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on principles of programming languages. ACM, New York, pp 52–66
Gondal A, Poppleton M, Snook C (2009) Feature composition—towards product lines of Event-B models. In: 1st International workshop on model-driven product line engineering. Twente, The Netherlands, pp 18–25
Gørtz J (1994) Specifying safety and progress properties with rsl. In: Naftalin M, Denvir T, Bertran M (eds) FME ’94: industrial benefit of formal methods. Lecture Notes in Computer Science, vol 873. Springer, Berlin, pp 567–581
TRL Group (1993) The RAISE specification language. Prentice-Hall Inc., Upper Saddle River
Hoare CAR (1985) Communicating sequential processes. Prentice Hall Int., Upper Saddle River
Jackson MA (1983) System development (Prentice-Hall International series in computer science). Prentice-Hall Inc., Upper Saddle River
Jones CB (1990) Systematic software development using VDM. 2nd edn. Prentice-Hall Inc., Upper Saddle River
Joochim T, Snook C, Poppleton M, Gravell A (2010) Timing diagrams requirements modeling using Event-B formal methods. In: IASTED international conference on software engineering (SE2010). Innsbruck, Austria
Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng 3(2):125–143 (1977). http://doi.ieeecomputersociety.org/10.1109/TSE.1977.229904
van Lamsweerde A (2009) Requirements engineering: from system goals to UML models to software specifications. Wiley, Chichester
Lanoix A (2008) Event-B specification of a situated multi-agent system: study of a platoon of vehicles. In: 2nd IFIP/IEEE international symposium on theoretical aspects of software engineering (TASE). IEEE Computer Society, pp 297–304
Leuschel M, Butler M (2003) ProB: a model checker for B. In: Araki K, Gnesi S, Mandrioli D (eds) FME 2003: formal methods, LNCS 2805. Springer, New York, pp 855–874
Mashkoor A, Jacquot JP (2009) Incorporating animation in stepwise development of formal specification. Research report INRIA-00392996, LORIA, Nancy, France (2009). http://hal.inria.fr/inria-00392996/en
Mashkoor A, Jacquot JP (2010) Transformational heuristics for animation—towards stepwise validation of specications. Research report HAL-00544261, LORIA, Nancy, France (2010). http://hal.archives-ouvertes.fr/hal-00544261/en/
Mashkoor A, Jacquot JP, Souquières J (2009) Transformation Heuristics for formal requirements validation by animation. In: 2nd International workshop on the certification of safety-critical software controlled systems—SafeCert ’09. York, UK
Mashkoor A, Jacquot JP, Souquières J (2009) B événementiel pour la modélisation du domaine: application au transport. In: Approches formelles dans l’Assistance au Développement de Logiciels (AFADL’2009), p 19. France Toulouse (2009). http://hal.inria.fr/inria-00326355/en/
Mashkoor A, Matoussi A (2010) Towards validation of requirements models. In: 2nd International conference on abstract state machines (ASM), Alloy, B and Z (ABZ ’10). Orford, Canada
Matoussi A, Gervais F, Laleau R (2008) A first attempt to express KAOS refinement patterns with event B. In: Proceedings of the International Conference on ASM, B and Z (ABZ). Lecture Notes in Computer Science. Springer, New York, pp 12–14
Milner R, Tofte M, Harper R, Macqueen D (1997) The definition of standard ML—revised. The MIT Press, Cambridge
Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: Kapur D (ed) 11th International conference on automated deduction (CADE). Lecture Notes in Artificial Intelligence, vol 607. Springer, Saratoga, NY, pp 748–752
Papatsaras A, Stoddart B (2002) Global and communicating state machine models in event driven b: a simple railway case study. In: ZB ’02: Proceedings of the 2nd international conference of B and Z users on formal specification and development in Z and B. Springer, London, pp 458–476
Poppleton M (2008) The composition of Event-B models. In: 1st International conference on ASM, B and Z (ABZ2008). London, UK
Schneider S, Treharne H, Wehrheim H (2010) A CSP approach to control in Event-B. In: Integrated formal methods-IFM 2010 integrated formal methods—8th international conference, IFM 2010, vol 6396. Springer, Berlin, pp 260–274
Servat T (2006) BRAMA: a new graphic animation tool for B models. In: B 2007: Formal specification and development in B. Springer, New York, pp 274–276
Silva R, Pascal C, Hoang T, Butler M (2010) Decomposition tool for Event-B. In: Workshop on tool building in formal methods. Orford, Canada
Snook C, Butler M (2006) UML-B: formal modeling and design aided by UML. ACM Trans Softw Eng Methodol 15(1):92–122
Yadav D, Butler M (2009) Verification of liveness properties in distributed systems. In: Second international conference on contemporary computing (IC3’09). Noida, India, pp 625–636
Yang F, Jacquot JP (2011) Scaling up with Event-B: a case study. In: Havelund K (ed) Proceedings of the 3rd NASA formal methods symposium (NFM2011), p. to appear. LNCS