Towards Model Checking Product Lines in the Digital Humanities: An Application to Historical Data
- 2 Citations
- 615 Downloads
Abstract
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.
Keywords
Digital humanities Big Data Interoperability Data integration Historical data Product lines CFMTS DIME Workflow processes Model checkingNotes
Acknowledgments
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 (www.lero.ie). We are grateful for the full cooperation of the Registrar General of Ireland for permission to use these data for research purposes.
References
- 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). http://tomheath.com/papers/bizer-heath-berners-lee-ijswis-linked-data.pdf
- 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.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.Kitchin, R.: Big data, new epistemologies and paradigm shifts’, Big Data & Society, pp. 1–12, April–June 2014. https://doi.org/10.1177/2053951714528481CrossRefGoogle Scholar
- 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.National Institute of Standards and Technology (NIST): U.S. Department of Commerce, Big Data Interoperability Framework, vol. 1, Definitions (2015)Google Scholar
- 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.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.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.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). https://doi.org/10.1007/978-3-319-47169-3_60CrossRefGoogle Scholar
- 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.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.Margaria, T.: Knowledge management for inclusive system evolution. Trans. Found. Mastering Chang. 1, 7–21 (2016)CrossRefGoogle Scholar
- 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.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.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). https://doi.org/10.1007/978-3-540-79450-9_42CrossRefGoogle Scholar
- 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.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.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). https://doi.org/10.1007/978-3-030-00244-2_15CrossRefGoogle Scholar
- 20.Steffen, B., Naujokat, S.: Archimedean points: the essence for mastering change. Trans. Found. Mastering Chang. 1, 22–46 (2016). https://doi.org/10.1007/978-3-319-46508-1_3CrossRefGoogle Scholar
- 21.Margaria, T., Steffen, B.: Simplicity as a driver for agile innovation. IEEE Comput. 43(6), 90–92 (2010). https://doi.org/10.1109/MC.2010.177CrossRefGoogle Scholar
- 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.Lamprecht, A.L., Margaria, T., Steffen, B.: Bio-jETI: a framework for semantics-based service composition. BMC Bioinformatics 10(10), S8 (2009). https://doi.org/10.1186/1471-2105-10-S10-S8CrossRefGoogle Scholar
- 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). https://doi.org/10.1007/978-3-319-42111-7_12CrossRefGoogle Scholar
- 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). https://doi.org/10.1109/LICS.1988.5119
- 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). https://doi.org/10.1007/3-540-60218-6_6CrossRefGoogle Scholar
- 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). https://doi.org/10.1186/1471-2105-9-S4-S12CrossRefGoogle Scholar
- 28.S. Gnesi, T. Margaria. Formal methods for industrial critical systems: A survey of applications. John Wiley & Sons, 2012. BookGoogle Scholar
- 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). https://doi.org/10.1007/978-3-662-45234-9_5CrossRefGoogle Scholar
- 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). https://doi.org/10.1007/978-3-540-88479-8_35CrossRefGoogle Scholar
- 31.Margaria, T., Steffen, B.: Service-Orientation: Conquering Complexity with XMDD. In: Hinchey, M., Coyle, L. (eds.) Conquering Complexity. Springer, London (2012). https://doi.org/10.1007/978-1-4471-2297-5_10CrossRefGoogle Scholar
- 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.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.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). https://doi.org/10.1007/978-3-540-24667-1_14CrossRefGoogle Scholar
- 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.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). https://doi.org/10.1007/978-3-642-21461-5_3CrossRefGoogle Scholar
- 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.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. https://doi.org/10.1109/SPLC.2011.34
- 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). https://doi.org/10.1007/BFb0084787CrossRefGoogle Scholar
- 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.An Act for the Registration of Births and Deaths in Ireland. 26 & 27 - Vict. c.11Google Scholar
- 42.Breathnach, C., O’Halpin, E.: Registered “unknown” infant fatalities in Ireland, 1916-1932. Ir. Hist. Stud. 38(149), 70–88 (2012). https://doi.org/10.1017/S0021121400000638CrossRefGoogle Scholar
- 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.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). https://doi.org/10.4204/eptcs.61.3CrossRefGoogle Scholar
- 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. https://doi.org/10.1109/inw.1997.601576