Towards Model Checking Product Lines in the Digital Humanities: An Application to Historical Data

Part of the Lecture Notes in Computer Science book series (LNCS, volume 11865)


Rapid development in computing techniques and databases’ systems have aided in the digitization of, and access to, various historical (big) data, with significant challenges of analysis and interoperability. The Death and Burial Data, Ireland project aims to build a Big Data interoperability framework loosely based on the Knowledge Discovery Data (KDD) process to integrate Civil Registration of Death data with other data types collated in Ireland from 1864 to 1922.

For our project, we resort to a Document Type Description (DTD) product line to represent and manage various representations and enrichments of the data. Well-formed documents serve as contracts between a provider (of the data set) and its customers (the researchers that consult them). We adopt the Context-Free Modal Transition Systems as a formalism to specify product lines of DTDs. The goal is to then proceed to product line verification using context-free model checking techniques, specifically the M3C checker of [14] to ensure that they are fit for purpose. The goal is to later implement and manage the corresponding family of data models and processes in the DIME framework, leveraging its flexible data management layer to define and efficiently manage the interoperable historical data framework for future use.

The resulting hierarchical product line verification will allow our technical platform to act as a high-quality service provider for digital humanities researchers, providing them with a wide range of tailored applications implementing the KDD process, whose essential business rules are easily checked by a standard DTD checker.


Digital humanities Big Data Interoperability Data integration Historical data Product lines CFMTS DIME Workflow processes Model checking 



This research is funded by the Irish Research Council Laureate Award 2017/2018 and by Science Foundation Ireland grant 13/RC/2094 to Lero - the Irish Software Research Centre ( We are grateful for the full cooperation of the Registrar General of Ireland for permission to use these data for research purposes.


  1. 1.
    Bizer, C., Heath, T., Berners-Lee, T.: Linked Data — the story so far. In: Hepp, M., Bizer, C.: (eds.) Special Issue on Linked Data, International Journal on Semantic Web and Information Systems, pp. 1–26 (2009).
  2. 2.
    Rose, N.: The politics of life itself: biomedicine, power, and subjectivity in the twenty-first century. Princeton University Press, Princeton (2007)CrossRefGoogle Scholar
  3. 3.
    Graham, S., Milligan, I., Weingart, S.: Big Digital History: Exploring Big Data through a Historian’s Macroscope. Imperial College Press, London (2015)CrossRefGoogle Scholar
  4. 4.
    Kitchin, R.: Big data, new epistemologies and paradigm shifts’, Big Data & Society, pp. 1–12, April–June 2014. Scholar
  5. 5.
    Ginzburg, C., Tedeschi, J., Tedeschi, A.C.: Microhistory: two or three things that i know about it. Crit. Inq. 20, 10–35 (1993)CrossRefGoogle Scholar
  6. 6.
    National Institute of Standards and Technology (NIST): U.S. Department of Commerce, Big Data Interoperability Framework, vol. 1, Definitions (2015)Google Scholar
  7. 7.
    Fayyad, U., Piatetsky-Shapiro, G., Smyth, P.: From data mining to knowledge discovery in databases. AI Mag. 17(3), 37–54 (1996)Google Scholar
  8. 8.
    Singh, R.K.: Taxonomy of big data analytics: methodology, algorithms and tools. Int. J. Future Revolution Comput. Sci. Commun. Eng. 4(12), 101–104 (2018)MathSciNetGoogle Scholar
  9. 9.
    Gyamfi, N.K., Appiah, P., Sarpong, K.A., Gah, S.K., Katsriku, F., Abdulai, J.: Big data analytics: survey paper. In: Conference Proceeding: Dialogue on Sustainability and Environmental Management, Accra, pp. 101–112, 15–16 February 2017Google Scholar
  10. 10.
    Boßelmann, S., et al.: DIME: a programming-less modeling environment for web applications. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 809–832. Springer, Cham (2016). Scholar
  11. 11.
    Naujokat, S., Lybecait, M., Kopetzki, D., Steffen, B.: CINCO: a simplicity-driven approach to full generation of domain-specific graphical modeling tools. Int. J. Softw. Tools Technol. Transfer 20, 327–354 (2018)CrossRefGoogle Scholar
  12. 12.
    Lamprecht, A.-L., Steffen, B., Margaria, T.: Scientific workflows with the jABC framework - a review after a decade in the field. STTT 18(6), 629–651 (2016)CrossRefGoogle Scholar
  13. 13.
    Margaria, T.: Knowledge management for inclusive system evolution. Trans. Found. Mastering Chang. 1, 7–21 (2016)CrossRefGoogle Scholar
  14. 14.
    Tegeler, T., Murtovi, A., Frohme, M., Steffen, B.: Product line verification via modal meta model checking. In: ter Beek, M.H., et al. (eds.) Gnesi Festschrift. LNCS, vol. 11865, pp. 313–337. Springer, Cham (2019)Google Scholar
  15. 15.
    Jörges, S., Lamprecht, A.L., Margaria, T., Schaefer, I., Steffen, B.: A constraint-based variability modeling framework. Int. J. Softw. Tools Technol. Transfer 14(5), 511–530 (2012)CrossRefGoogle Scholar
  16. 16.
    Lamprecht, A.-L., Margaria, T., Steffen, B.: Seven variations of an alignment workflow - an illustration of agile process design and management in bio-jETI. In: Măndoiu, I., Sunderraman, R., Zelikovsky, A. (eds.) ISBRA 2008. LNCS, vol. 4983, pp. 445–456. Springer, Heidelberg (2008). Scholar
  17. 17.
    Karusseit, M., Margaria, T.: Feature-based modelling of a complex, online-reconfigurable decision support service. Electron. Notes Theor. Comput. Sci. 157(2), 101–118 (2006)CrossRefGoogle Scholar
  18. 18.
    Steffen, B., Gossen, F., Naujokat, S., Margaria, T.: Language-driven engineering: from general-purpose to purpose-specific languages. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science: State of the Art and Perspectives. LNCS, vol. 10000. Springer (2018, in print)Google Scholar
  19. 19.
    Steffen, B., Murtovi, A.: M3C: modal meta model checking. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 223–241. Springer, Cham (2018). Scholar
  20. 20.
    Steffen, B., Naujokat, S.: Archimedean points: the essence for mastering change. Trans. Found. Mastering Chang. 1, 22–46 (2016). Scholar
  21. 21.
    Margaria, T., Steffen, B.: Simplicity as a driver for agile innovation. IEEE Comput. 43(6), 90–92 (2010). Scholar
  22. 22.
    Margaria, T., Lamprecht, A.L., Steffen, B.: Continuous Model-Driven Engineering. Software Technology: 10 Years of Innovation in IEEE Computer, pp. 141–154. Wiley (2018)Google Scholar
  23. 23.
    Lamprecht, A.L., Margaria, T., Steffen, B.: Bio-jETI: a framework for semantics-based service composition. BMC Bioinformatics 10(10), S8 (2009). Scholar
  24. 24.
    Al-Areqi, S., Lamprecht, A.-L., Margaria, T.: Constraints-driven automatic geospatial service composition: workflows for the analysis of sea-level rise impacts. In: Gervasi, O., et al. (eds.) ICCSA 2016. LNCS, vol. 9788, pp. 134–150. Springer, Cham (2016). Scholar
  25. 25.
    Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings. Third Annual Symposium on Logic in Computer Science, pp. 203–210. IEEE (1988).
  26. 26.
    Steffen, B., Claßen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 72–87. Springer, Heidelberg (1995). Scholar
  27. 27.
    Margaria, T., Kubczak, C., Steffen, B.: Bio-jETI: a service integration, design, and provisioning platform for orchestrated bioinformatics processes. BMC Bioinformatics 9(4), S12 (2008). Scholar
  28. 28.
    S. Gnesi, T. Margaria. Formal methods for industrial critical systems: A survey of applications. John Wiley & Sons, 2012. BookGoogle Scholar
  29. 29.
    Neubauer, J., Frohme, M., Steffen, B., Margaria, T.: Prototype-driven development of web applications with DyWA. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8802, pp. 56–72. Springer, Heidelberg (2014). Scholar
  30. 30.
    Margaria, T., Steffen, B.: Agile IT: thinking in user-centric models. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 490–502. Springer, Heidelberg (2008). Scholar
  31. 31.
    Margaria, T., Steffen, B.: Service-Orientation: Conquering Complexity with XMDD. In: Hinchey, M., Coyle, L. (eds.) Conquering Complexity. Springer, London (2012). Scholar
  32. 32.
    Lamprecht, A.L., Margaria, T., Steffen, B., Sczyrba, A., Hartmeier, S., Giegerich, R.: GeneFisher-P: variations of GeneFisher as processes in Bio-jETI. BMC bioinformatics 9(4), 1–17 (2008). S13Google Scholar
  33. 33.
    Al-areqi, S., Lamprecht, A.L., Margaria, T., Kriewald, S., Reusser, D., Wrobel, M.: Agile workflows for climate impact risk assessment based on the ci: grasp platform and the jABC modeling framework. In: 7th International Congress on Environmental Modelling and Software, International Environmental Modelling and Software Society (iEMSs), pp. 470–477 (2014)Google Scholar
  34. 34.
    Bertolino, A., Gnesi, S.: PLUTO: a test methodology for product families. In: van der Linden, F.J. (ed.) PFE 2003. LNCS, vol. 3014, pp. 181–197. Springer, Heidelberg (2004). Scholar
  35. 35.
    Bertolino, A., Fantechi, A., Gnesi, S., Lami, G., Maccari, A.: Use case description of requirements for product lines. In: Proceedings of the International Workshop on Requirements Engineering for Product Lines - REPL 2002. Technical report: ALR2002-033, AVAYA, pp. 12–18 (2002)Google Scholar
  36. 36.
    Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A model-checking tool for families of services. In: Bruni, R., Dingel, J. (eds.) FMOODS/FORTE -2011. LNCS, vol. 6722, pp. 44–58. Springer, Heidelberg (2011). Scholar
  37. 37.
    ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J. Log. Algebraic Methods Program. 85(2), 287–315 (2016)MathSciNetCrossRefGoogle Scholar
  38. 38.
    Asirelli, P., ter Beek, M.H., Gnesi, S., Fantechi, A.: Formal description of variability in product families. In: 15th International Software Product Line Conference, pp. 130–139, August 2011.
  39. 39.
    Burkart, O., Steffen, B.: Model checking for context-free processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 123–137. Springer, Heidelberg (1992). Scholar
  40. 40.
    Blackburn, P., van Benthem, J.F.A.K., Wolter, F.: Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3. Elsevier Science Inc., New York (2006)CrossRefGoogle Scholar
  41. 41.
    An Act for the Registration of Births and Deaths in Ireland. 26 & 27 - Vict. c.11Google Scholar
  42. 42.
    Breathnach, C., O’Halpin, E.: Registered “unknown” infant fatalities in Ireland, 1916-1932. Ir. Hist. Stud. 38(149), 70–88 (2012). Scholar
  43. 43.
    Basile, D., ter Beek, M.H., Gnesi, S.: Modelling and analysis with featured modal contract automata. SPLC 2, 11–16 (2018)CrossRefGoogle Scholar
  44. 44.
    ter Beek, M.H., Gnesi, S., Njima, M.N.: Product lines for service oriented applications - PL for SOA. In: Kovács, L., Pugliese, R., Tiezzi, F. (eds.) Proceedings 7th International Workshop on Automated Specification and Verification of Web Systems (WWV 2011) (EPTCS), vol. 61, pp. 34–48. Open Publishing Association (2011). Scholar
  45. 45.
    Braun, V., Margaria, T., Steffen, B., Yoo, H., Rychly, T.: safe service customization. In: Proceedings of the IEEE Intelligent Network Workshop: ‘Meeting the Challenges of Converging Networks and Global Demand’. IEEE, May 1997.

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Department of HistoryHealth Research Institute and LeroDublinIreland
  2. 2.Department of Computer Science and Information Systems, Lero and HRIUniversity of LimerickLimerickIreland

Personalised recommendations