nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

22.02.2019 | Regular Paper

Spatial logics and model checking for medical imaging

verfasst von: Fabrizio Banci Buonamici, Gina Belmonte, Vincenzo Ciancia, Diego Latella, Mieke Massink

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 2/2020

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Recent research on spatial and spatio-temporal model checking provides novel image analysis methodologies, rooted in logical methods for topological spaces. Medical imaging (MI) is a field where such methods show potential for ground-breaking innovation. Our starting point is SLCS, the Spatial Logic for Closure Spaces—closure spaces being a generalisation of topological spaces, covering also discrete space structures—and topochecker, a model checker for SLCS (and extensions thereof). We introduce the logical language ImgQL (“Image Query Language”). ImgQL extends SLCS with logical operators describing distance and region similarity. The spatio-temporal model checker topochecker is correspondingly enhanced with state-of-the-art algorithms, borrowed from computational image processing, for efficient implementation of distance-based operators, namely distance transforms. Similarity between regions is defined by means of a statistical similarity operator, based on notions from statistical texture analysis. We illustrate our approach by means of an example of analysis of Magnetic Resonance images: segmentation of glioblastoma and its oedema.

Vorheriger Artikel A greedy particle swarm optimization (GPSO) algorithm for testing real-world smart card applications

Nächster Artikel A formal approach to AADL model-based software engineering

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

This is witnessed by current results that are publicly evaluated in the latest editions of the multimodal brain tumour image segmentation benchmark (BraTS), see https://www.cbica.upenn.edu/sbia/Spyridon.Bakas/MICCAI_BraTS/MICCAI_BraTS_2017_proceedings_shortPapers.pdf.

Topochecker: a topological model checker, see http://topochecker.isti.cnr.it, https://github.com/vincenzoml/topochecker.

In the caption, such a closure is abbreviated by \({\mathcal {C}}_{R}(blue)\) for space reasons.

The size of a formula is given by the number of operators in the formula: \(size(p)=1; size(\lnot \varPhi )=size({\mathcal {N}}\varPhi )=1+size(\varPhi ); size(\varPhi _1 \wedge \varPhi _2)=size(\varPhi _1 {\mathcal {S}}\;\varPhi _2)=1+size(\varPhi _1)+ size(\varPhi _2)\).

In image processing, the problem of co-registration is that of mapping two images coming from different sources to the same spatial domain, by finding transformations of the considered images that make given image features coincide.

See https://github.com/vincenzoml/topochecker.

See http://www.ocaml.org.

Available for download at https://github.com/vincenzoml/spatial-model-checking-benchmarks.

Vasogenic oedema is an abnormal accumulation of fluid from blood vessels, which is able to disrupt the blood–brain barrier and invade extracellular space.

To ease visual comparison, in Figs. 16d, 17d, 18b, the histograms that we show are normalised so that the measure of the area below the curve is 1.

For instance, jpeg images, as downloaded from Radiopaedia.org, typically use 8-bit precision (typical range 0-255) (see Fig. 16), whereas dicom images saved by scanners typically use 12 or 16-bit (for MR images, the typical range is 0–4096 or 0–65536, respectively) (see Fig. 18).

Adams, R., Bischof, L.: Seeded region growing. IEEE Trans. Pattern Anal. Mach. Intell. 16, 641–647 (1994)CrossRef

Aiello, M.: Spatial Reasoning: Theory and Practice. Ph.D. thesis, Institute of Logic, Language and Computation, University of Amsterdam (2002)

Aiello, M., Pratt-Hartmann, I., van Benthem, J.: Handbook of Spatial Logics. Springer, New York (2007)CrossRefMATH

Akkus, Z., Galimzianova, A., Hoogi, A., Rubin, D.L., Erickson, B.J.: Deep learning for brain mri segmentation: state of the art and future directions. J. Digit. Imaging 30, 449–459 (2017)CrossRef

Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spatially distributed cyber-physical systems. In: Talpin, J.P., Derler, P., Schneider, K. (eds.) Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017, Vienna, Austria, September 29–October 02, 2017, pp. 146–155. ACM, New York (2017)

Bartocci, E., Bortolussi, L., Milios, D., Nenzi, L., Sanguinetti, G.: Studying emergent behaviours in morphogenesis using signal spatio-temporal logic. In: Hybrid Systems Biology: Fourth International Workshop, HSB 2015, Madrid, Spain, September 4–5, 2015. Revised Selected Papers, pp. 156–172. Springer (2015)

Bartocci, E., Gol, E.A., Haghighi, I., Belta, C.: A formal methods approach to pattern recognition and synthesis in reaction diffusion networks. IEEE Trans. Control Netw. Syst. 5(1), 308–320 (2018)CrossRefMathSciNetMATH

Bauer, S., Wiest, R., Nolte, L.-P., Reyes, M.: A survey of MRI-based medical image analysis for brain tumor studies. Phys. Med. Biol. 58(13), R97 (2013)CrossRef

Belmonte, G., Ciancia, V., Latella, D., Massink, M.: From collective adaptive systems to human centric computation and back: spatial model checking for medical imaging. In: ter Beek, M., Loreti, M. (eds.) Proceedings of the Workshop on FORmal Methods for the Quantitative Evaluation of Collective Adaptive SysTems, FORECAST@STAF 2016, Vienna, Austria, 8 July 2016, Volume 217 of EPTCS, pp. 81–92 (2016)

10.

Belmonte, G., Ciancia, V., Latella, D., Massink, M.: Voxlogica: a spatial model checker for declarative image analysis. In: Tools and Algorithms for the Construction and Analysis of Systems—25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, Logical Methods in Computer Science. Springer (to appear) (2019)

11.

Belmonte, G., Ciancia, V., Latella, D., Massink, M., Biondi, M., De Otto, G., Nardone, V., Rubino, G., Vanzi, E., Banci Buonamici, F.: A topological method for automatic segmentation of glioblastoma in MR air for radio-therapy—ESMRMB 2017, 34th annual scientific meeting. Magn. Reson. Mater. Phys. Biol. Med. 30(S1), 437 (2017)

12.

Brock, K.: Image Processing in Radiation Therapy. CRC Press, Boca Raton (2014)

13.

Brown, L.: A survey of image registration techniques. ACM Comput. Surv. 24(4), 325–376 (1992)CrossRef

14.

Brown, R., Cheng, N., Haacke, E., Thompson, M., Venkatesan, R. (eds.): Magnetic Resonance Imaging. Wiley, New York (2014)

15.

Burnet, N.: Defining the tumour and target volumes for radiotherapy. Cancer Imaging 4(2), 153–161 (2004)CrossRef

16.

Castellano, G., Bonilha, L., Li, L., Cendes, F.: Texture analysis of medical images. Clin. Radiol. 59(12), 1061–1069 (2004)CrossRef

17.

Chen, C., Da Ponte, J., Fox, M.: Fractal feature analysis and classification in medical imaging. IEEE Trans. Med. Imaging 8(2), 133–142 (1989)CrossRef

18.

Chetelat, G., Baron, J.: Early diagnosis of alzheimer’s disease: contribution of structural neuroimaging. NeuroImage 18(2), 525–541 (2003)CrossRef

19.

Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. Int. J. Softw. Tools Technol. Transf. 20(3), 289–311 (2018)CrossRef

20.

Ciancia, V., Gilmore, S., Latella, D., Loreti, M., Massink, M.: Data verification for collective adaptive systems: spatial model-checking of vehicle location data. In: Eighth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASOW, pp. 32–37. IEEE Computer Society (2014)

21.

Ciancia, V., Grilletti, G., Latella, D., Loreti, M., and Massink, M.: An experimental spatio-temporal model checker. In: Software Engineering and Formal Methods—SEFM 2015 Collocated Workshops, Volume 9509 of Lecture Notes in Computer Science, pp. 297–311. Springer (2015)

22.

Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: Theoretical Computer Science—8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1–3, 2014. Proceedings, Volume 8705 of Lecture Notes in Computer Science, pp. 222–235. Springer (2014)

23.

Ciancia, V., Latella, D., Loreti, M., Massink, M.: Model checking spatial logics for closure spaces. Log. Methods Comput. Sci. 12(4), 1–51 (2016)MathSciNetMATH

24.

Ciancia, V., Latella, D., Loreti, M., Massink, M.: Spatial logic and spatial model checking for closure spaces. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems—16th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2016, Bertinoro, Italy, June 20–24, 2016, Advanced Lectures, Volume 9700 of Lecture Notes in Computer Science, pp. 156–201. Springer, New York (2016)

25.

Ciancia, V., Latella, D., Massink, M., Pakauskas, R.: Exploring spatio-temporal properties of bike-sharing systems. In: 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASO Workshops, pp. 74–79. IEEE Computer Society (2015)

26.

Ciancia, V., Latella, D., Massink, M., Paskauskas, R., Vandin, A.: A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques—7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I, Volume 9952 of Lecture Notes in Computer Science, pp. 657–673 (2016)

27.

Ciesielski, K., Chen, X., Udupa, J., Grevera, G.: Linear time algorithms for exact distance transform. J. Math. Imaging Vis. 39(3), 193–209 (2010)CrossRefMathSciNetMATH

28.

Clarke, E., Emerson, A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, Workshop, pp. 52–71. Springer, London (1982)

29.

Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Boca Raton (1999)MATH

30.

Davnall, F., Yip, C., Ljungqvist, G., Selmi, M., Ng, F., Sanghera, B., Ganeshan, B., Miles, K.A., Cook, G.J., Goh, V.: Assessment of tumor heterogeneity: an emerging imaging tool for clinical practice? Insights Imaging 3(6), 573–589 (2012)CrossRef

31.

De Nicola, R., Katoen, J., Latella, D., Loreti, M., Massink, M.: Model checking mobile stochastic logic. Theor. Comput. Sci. 382(1), 42–70 (2007)CrossRefMathSciNetMATH

32.

De Santis, S., Drakesmith, M., Bells, S., Assaf, Y., Jones, D.: Why diffusion tensor MRI does well only some of the time: variance and covariance of white matter tissue microstructure attributes in the living human brain. NeuroImage 89, 35–44 (2014)CrossRef

33.

Despotović, I., Goossens, B., Philips, W.: MRI segmentation of the human brain: challenges, methods, and applications. Comput. Math. Methods Med. 1–23, 2015 (2015)

34.

Doi, K.: Computer-aided diagnosis in medical imaging: historical review, current status and future potential. Comput. Med. Imaging Graph. 31(4–5), 198–211 (2007)CrossRef

35.

Dupont, C., Betrouni, N., Reyns, Vermandel, M.: On image segmentation methods applied to glioblastoma: state of art and new trends. IRBM 37(3), 131–143 (2016)CrossRef

36.

Fabbri, R., Costa, L., Torelli, J., Odemir, B.: 2D Euclidean distance transform algorithms: a comparative survey. ACM Comput. Surv. 40(1), 2:1–2:44 (2008)CrossRef

37.

Fabbri, R., Da Fontoura Da Costa, L., Torelli, J., Bruno, O.: 2D Euclidean distance transform algorithms: a comparative survey. ACM Comput. Surv. 40(1), 2:1–2:44 (2008)CrossRef

38.

Fyllingen, E., Stensjøen, A., Berntsen, E., Solheim, O., Reinertsen, I.: Glioblastoma segmentation: comparison of three different software packages. PLoS ONE 11(10), e0164891 (2016)CrossRef

39.

Galton, A.: The mereotopology of discrete space. In: Freksa, C., David, M. (eds.) Spatial Information Theory. Cognitive and Computational Foundations of Geographic Information Science, Volume 1661 of Lecture Notes in Computer Science, pp. 251–266. Springer, Berlin (1999)

40.

Galton, A.: A generalized topological view of motion in discrete space. Theor. Comput. Sci. 305(1–3), 111–134 (2003)CrossRefMathSciNetMATH

41.

Galton, A.: Discrete mereotopology. In: Calosi, C., Graziani, P. (eds.) Mereology and the Sciences: Parts and Wholes in the Contemporary Scientific Context, pp. 293–321. Springer, New York (2014)

42.

Gol, E., Bartocci, E., Belta, C.: A formal methods approach to pattern synthesis in reaction diffusion systems. In: 53rd IEEE Conference on Decision and Control, pp. 108–113 (2014)

43.

Gordillo, N., Montseny, E., Sobrevilla, E.: State of the art survey on MRI brain tumor segmentation. Magn. Reson. Imaging 31(8), 1426–1438 (2013)CrossRef

44.

Grevera, G.: Distance transform algorithms and their implementation and evaluation. In: Farag, A.A., Suri, J.S. (eds.) Deformable Models, pp. 33–60. Springer (2007)

45.

Grosu, R., Smolka, S., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), 97–105 (2009)CrossRefMATH

46.

Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Grosu, R., Belta, C.: Spatel: A novel spatial-temporal logic and its applications to networked systems. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC ’15, pp. 189–198. ACM, New York (2015)

47.

Han, F., Wang, H., Zhang, G., Han, H., Song, B., Li, L., Moore, W., Lu, H., Zhao, H., Liang, Z.: Texture feature analysis for computer-aided diagnosis on pulmonary nodules. J. Digit. Imaging 28(1), 99–115 (2014)CrossRef

48.

Haralick, R., et al.: Textural features for image classification. IEEE Trans. Syst. Man Cybern. 3(6), 610–621 (1973)CrossRef

49.

Heinonen, T., Arola, T., Kalliokoski, A., Dastidar, P., Rossi, M., Soimakallio, S., Hyttinen, J., Eskola, H.: Computer aided diagnosis tool for the segmentation and texture analysis of medical images. In: IFMBE Proceedings, pp. 274–276. Springer (2009)

50.

Kassner, A., Thornhill, R.: Texture analysis: a review of neurologic MR imaging applications. Am. J. Neuroradiol. 31(5), 809–816 (2010)CrossRef

51.

Kimmel, R., Kiryati, N., Bruckstein, A.: Sub-pixel distance maps and weighted distance transforms. J. Math. Imaging Vis. 6(2), 223–233 (1996)CrossRefMathSciNet

52.

Kontchakov, R., Kurucz, A., Wolter, F., Zakharyaschev, M.: Spatial logic + temporal logic = ? In: Aiello, M., Pratt-Hartmann, I. , van Benthem, J. (eds.) Handbook of Spatial Logics, pp. 497–564. Springer (2007)

53.

Kutz, O., Wolter, F., Sturm, H., Suzuki, N., Zakharyaschev, M.: Logics of metric spaces. ACM Trans. Comput. Log. 4(2), 260–294 (2003)CrossRefMathSciNetMATH

54.

Lemieux, L., Hagemann, G., Krakow, K., Woermann, F.: Fast, accurate, and reproducible automatic segmentation of the brain in T1-weighted volume MRI data. Magn. Reson. Med. 42(1), 127–135 (1999)CrossRef

55.

Li, C., Herndon, J., Novembre, F., Zhang, X.: A longitudinal magnetization transfer imaging evaluation of brain injury in a macaque model of NeuroAIDS. AIDS Res. Hum. Retrovir. 31(3), 335–341 (2015)CrossRef

56.

Lopes, R., Ayache, A., Makni, N., Puech, P., Villers, A., Mordon, S., Betrouni, N.: Prostate cancer characterization on MR images using fractal features. Med. Phys. 38(1), 83 (2011)CrossRef

57.

Madabhushi, A., Udupa, J.: New methods of MR image intensity standardization via generalized scale. Med. Phys. 33(9), 3426–3434 (2006)CrossRef

58.

Maurer, C., Rensheng, Q., Raghavan, V.: A linear time algorithm for computing exact euclidean distance transforms of binary images in arbitrary dimensions. IEEE Trans. Pattern Anal. Mach. Intell. 25(2), 265–270 (2003)CrossRef

59.

Mazzara, G., Velthuizen, R., Pearlman, J., Greenberg, H., Wagner, H.: Brain tumor target volume determination for radiation treatment planning through automated MRI segmentation. Int. J. Radiat. Oncol. Biol. Phys. 59(1), 300–312 (2004)CrossRef

60.

Menze, B., et al.: The multimodal brain tumor image segmentation benchmark (brats). IEEE Trans. Med. Imaging 34(10), 1993–2024 (2015)CrossRef

61.

Meshgi, K., Ishii, S.: Expanding histogram of colors with gridding to improve tracking accuracy. In: MVA (2015)

62.

Mohan, G., Subashini, M.M.: Mri based medical image analysis: survey on brain tumor grade classification. Biomed. Signal Process. Control 39, 139–161 (2018)CrossRef

63.

Nenzi, L., Bortolussi, L.: Specifying and monitoring properties of stochastic spatio-temporal systems in signal temporal logic. In: 8th International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2014, Bratislava, Slovakia, December 9–11, 2014. ICST (2014)

64.

Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties. In: Runtime Verification—6th International Conference, RV 2015 Vienna, Austria, September 22–25, 2015. Proceedings, Volume 9333 of Lecture Notes in Computer Science, pp. 21–37. Springer (2015)

65.

Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties with SSTL. Log. Methods Comput. Sci. 14(4), 1–38 (2018). https://doi.org/10.23638/LMCS-14(4:2)2018 MathSciNetCrossRefMATH

66.

Prvu, O., Gilbert, D.: A novel method to verify multilevel computational models of biological systems using multiscale spatio-temporal meta model checking. PLoS ONE 11(5), 1–43 (2016). 05

67.

Reif, J., Sistla, A.: A multiprocess network logic with temporal and spatial modalities. J. Comput. Syst. Sci. 30(1), 41–53 (1985)CrossRefMathSciNetMATH

68.

Rengier, F., Mehndiratta, A., von Tengg-Kobligk, H., Zechmann, C.M., Unterhinninghofen, R., Kauczor, H.-U., Giesel, F.L.: 3D printing based on imaging data: review of medical applications. Int. J. Comput. Assist. Radiol. Surg. 5(4), 335–341 (2010)CrossRef

69.

Rodriguez Gutierrez, D., Awwad, A., Meijer, L., Manita, M., Jaspan, T., Dineen, R., Grundy, R., Auer, D.: Metrics and textural features of MRI diffusion to improve classification of pediatric posterior fossa tumors. Am. J. Neuroradiol. 35(5), 1009–1015 (2013)CrossRef

70.

Sharma, N., Ray, A., Sharma, S., Shukla, K., Pradhan, S., Aggarwal, L.: Segmentation and classification of medical images using texture-primitive features: application of BAM-type artificial neural network. J. Med. Phys. 33(3), 119 (2008)CrossRef

71.

Sheremet, M., Wolter, F., Zakharyaschev, M.: A modal logic framework for reasoning about comparative distances and topology. Ann. Pure Appl. Log. 161(4), 534–559 (2010)CrossRefMathSciNetMATH

72.

Simi, V., Joseph, J.: Segmentation of glioblastoma multiforme from MR images—a comprehensive review. Egypt. J. Radiol. Nucl. Med. 46(4), 1105–1110 (2015)CrossRef

73.

Srinivasan, G., Shobha, G.: Statistical texture analysis. Proc. World Acad. Sci. Eng. Technol. 36, 1264–1269 (2012)

74.

Sundstrom, A., Grabocka, E., Bar-Sagi, D., Mishra, B.: Histological image processing features induce a quantitative characterization of chronic tumor hypoxia. PLoS ONE 11(4), 1–30 (2016). 04CrossRef

75.

Thorup, M.: Undirected single-source shortest paths with positive integer weights in linear time. J. ACM 46(3), 362–394 (1999)CrossRefMathSciNetMATH

76.

Tijms, B., Series, P., Willshaw, D., Lawrie, S.: Similarity-based extraction of individual networks from gray matter MRI scans. Cereb. Cortex 22(7), 1530–1541 (2011)CrossRef

77.

Toosy, A.: Diffusion tensor imaging detects corticospinal tract involvement at multiple levels in amyotrophic lateral sclerosis. J. Neurol. Neurosurg. Psychiatry 74(9), 1250–1257 (2003)CrossRef

78.

van Benthem, J., Bezhanishvili, G.: Modal logics of space. In: Aiello, M., Pratt-Hartmann, I. , van Benthem, J. (eds.) Handbook of Spatial Logics, pp. 217–298. Springer (2007)

79.

Woods, B., Clymer, B., Kurc, T., Heverhagen, J., Stevens, R., Orsdemir, A., Bulan, O., Knopp, M.: Malignant-lesion segmentation using 4D co-occurrence texture analysis applied to dynamic contrast-enhanced magnetic resonance breast image data. J. Magn. Reson. Imaging 25(3), 495–501 (2007)CrossRef

80.

Zhu, Y., Young, G., Xue, Z., Huang, R., You, H., Setayesh, K., Hatabu, H., Cao, F., Wong, S.: Semi-automatic segmentation software for quantitative clinical brain glioblastoma evaluation. Acad. Radiol. 19(8), 977–985 (2012)CrossRef

Titel: Spatial logics and model checking for medical imaging
verfasst von: Fabrizio Banci Buonamici
Gina Belmonte
Vincenzo Ciancia
Diego Latella
Mieke Massink
Publikationsdatum: 22.02.2019
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 2/2020
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-019-00511-9

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 2/2020

A formal approach to AADL model-based software engineering

A greedy particle swarm optimization (GPSO) algorithm for testing real-world smart card applications

IC3 software model checking

Model-based testing of apps in real network scenarios

Joint forces for memory safety checking revisited

Introduction to the Special Issue devoted to SPIN 2018

Premium Partner