×

Analysing sanity of requirements for avionics systems. (English) Zbl 1335.68131


MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
93C95 Application models in control theory

Software:

RATSY; mCRL; NuSMV; iFEST; DiVinE; mCRL2
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Abadi M, Lamport L, Wolper P (1989) Realizable and unrealizable specifications of reactive systems. In: Proceedings of ICALP, pp 1-17
[2] Bormann J, Busch H (2009) Method for the determination of the quality of a set of properties, usable for the verification and specification of circuits. U. S. Patent No. 7,571,398 B2
[3] Barnat J, Bauch P, Brim L (2012) Checking sanity of software requirements. In: Proceedings of SEFM, pp 48-52
[4] Barnat J, Beran J, Brim L, Kratochvíla T, Ročkai P (2012) Tool chain to support automated formal verification of avionics simulink designs. In: Proceedings of FMICS, pp 78-92 · Zbl 1010.68766
[5] Barnat J, Brim L, Češka M, Ročkai P (2010) DiVinE: parallel distributed model checker. In: Proceedings of HiBi/PDMC, pp 4-7
[6] Beer I, Ben-David S, Eisner C, Rodeh Y (2001) Efficient detection of vacuity in temporal model checking. Form. Methods Syst. Des 18(2): 141-163 · Zbl 0988.68111 · doi:10.1023/A:1008779610539
[7] Bloem R, Cimatti A, Greimel K, Hofferek G, Könighofer R, Roveri M, Schuppan V, Seeber R (2010) RATSY—a new requirements analysis tool with synthesis. In: Proceedings of CAV, pp 425-429
[8] Blom, S.; Fokkink, W.; Groote, J.; Langevelde, I.; Lisser, B.; Pol, J., μCRL: a toolset for analysing algebraic specifications, 250-254 (2001), New York · Zbl 0991.68640
[9] Chan W, Anderson RJ, Bea P, Burns S, Modugno F, Notkin D, Reese JD (1989) Model checking large software specifications. IEEE Trans. Softw Eng 24: 498-520 · doi:10.1109/32.708566
[10] Cimatti, A.; Clarke, EM; Giunchiglia, E.; Giunchiglia, F.; Pistore, M.; Roveri, M.; Sebastiani, R.; Tacchella, A., NuSMV 2: an opensource tool for symbolic model checking, 241-268 (2002), New York · Zbl 1010.68766
[11] Chockler, H.; Kupferman, O.; Kurshan, R.; Vardi, MY, A practical approach to coverage in model checking, 66-78 (2001), New York · Zbl 0991.68042
[12] Chockler, H.; Kupferman, O.; Vardi, MY, Coverage metrics for temporal logic model checking, 528-542 (2001), New York · Zbl 0978.68092
[13] Cimatti A, Roveri M, Schuppan V, Tchaltsev A (2008) Diagnostic information for realizability. In: Proceedings of VMCAI, pp 52-67 · Zbl 1138.68442
[14] Courcoubetis C, Vardi MY, Wolper P, Yannakakis M (1992) Memory-efficient algorithms for the verification of temporal properties. Form. Method Syst. Des 1: 275-288 · Zbl 0786.68060 · doi:10.1007/BF00121128
[15] Dwyer MB, Avrunin GS, Corbett JC (1998) Property specification patterns for finite-state verification. In: Proceedings of FMSP, pp 7-15
[16] Duret-Lutz A (2011) LTL translation improvements in spot. In: Proceedings of VECoS, pp 72-83 · Zbl 0988.68111
[17] Feierbach G, Gupta V (2003) True coverage: a goal of verification. In: Proceedings of ISQED, pp 75-78 · Zbl 1154.68510
[18] Hinchey M, Jackson M, Cousot P, Cook B, Bowen JP, Margaria T (2008) Software engineering and formal methods. Communun. ACM 51: 54-59 · doi:10.1145/1378727.1378742
[19] Heimdahl MPE, Leveson NG (1995) Completeness and consistency analysis of state-based requirements. In: Proceedings of ICSE, pp 3-14
[20] Katz S, Grumberg O, Geist D (1999) “Have I Written Enough Properties?”—a method of comparison between specification and implementation. In: Proceedings of CHARME, pp 280-297 · Zbl 0957.68069
[21] Konighofer R, Hofferek G, Bloem R (2009) Debugging formal specifications using simple counterstrategies. In: Proceedings of FMCAD, pp 152-159 · Zbl 1151.68485
[22] Kupferman, O., Sanity checks in formal verification, 37-51 (2006), New York · Zbl 1151.68485
[23] Kupferman O, Vardi MY (2003) Vacuity detection in temporal model checking. STTT 4: 224-233 · Zbl 0961.68085 · doi:10.1007/s100090100062
[24] Leveson N (2000) Completeness in formal specification language design for process-control systems. In: Proceedings of FMSP, pp 75-87 · Zbl 1154.68510
[25] Lynce I, Marques-Silva JP (2004) On computing minimum unsatisfiable cores. In: Proceedings of SAT, pp 305-310 · Zbl 0786.68060
[26] Liffiton M, Sakallah K (2008) Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1): 1-33 · Zbl 1154.68510 · doi:10.1007/s10817-007-9084-z
[27] Miller, SP; Tribble, AC; Heimdahl, MPE, Proving the shalls, 75-93 (2003), New York
[28] Roy S, Das S, Basu P, Dasgupta P, Chakrabarti PP (2005) SAT based solutions for consistency problems in formal property specifications for open systems. In: Proceedings of ICCAD, pp 885-888
[29] Regimbal S, Lemire J-F, Savaria Y, Bois G, Aboulhamid E, Baron A (2003) Automating functional coverage analysis based on an executable specification. In Proceedings of IWSOC, pp 228-234 · Zbl 0991.68042
[30] Rozier, K.; Vardi, MY, LTL satisfiability checking, 149-167 (2007), New York
[31] Rajan A, Whalen MW, Heimdahl MPE (2007) Model validation using automatically generated requirements-based tests. In: Proceedings of HASE, pp 95-104
[32] Schuppan V (2012) Towards a notion of unsatisfiable and unrealizable cores for LTL. Sci. Comput. Program 77(7-8): 908-939 · Zbl 1242.68075 · doi:10.1016/j.scico.2010.11.004
[33] Tasiran S, Keutzer K (2001) Coverage metrics for functional validation of hardware designs. IEEE Des. Test. Comput 18(4): 36-45 · doi:10.1109/54.936247
[34] Whalen MW, Rajan A, Heimdahl MPE, Miller SP (2006) Coverage metrics for requirements-based testing. In: Proceedings of ISSTA, pp 25-36
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.