Skip to main content
SpringerLink
Log in
Book cover

International Conference on Software Engineering and Formal Methods

SEFM 2011: Software Engineering and Formal Methods pp 3–18Cite as

Formal Methods as a Link between Software Code and Legal Rules

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7041))

Abstract

The rapid evolution of the technological landscape and the impact of information technologies on our everyday life raise new challenges which cannot be tackled by a purely technological approach. Generally speaking, legal and technical means should complement each other to reduce risks for citizens and consumers : on one side, laws (or contracts) can provide assurances which are out of reach of technical means (or cope with situations where technical means would be defeated); on the other side, technology can help enforce legal and contractual commitments. This synergy should not be taken for granted however, and if legal issues are not considered from the outset, technological decisions made during the design phase may very well hamper or make impossible the enforcement of legal rights. But the consideration of legal constraints in the design phase is a challenge in itself, not least because of the gap between the legal and technical communities and the difficulties to establish a common understanding of the concepts at hand. In this paper, we advocate the use of formal methods to reduce this gap, taking examples in areas such as privacy, liability and compliance.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Anciaux, N., Benzine, M., Bouganim, L., Jacquemin, K., Pucheral, P., Yin, S.: Restoring the patient control over her medical history. In: 21st IEEE International Symposium on Computer-Based Medical Systems, pp. 132–137. IEEE Computer Society, Los Alamitos (2008)

    Chapter  Google Scholar 

  2. Anderson, R., Moore, T.: Information security economics – and beyond. Information Security Summit (IS2) (2009)

    Google Scholar 

  3. Balasch, J., Rial, A., Troncoso, C., Geuens, C., Preneel, B., Verbauwhede, I.: PrETP: privacy-preserving electronic toll pricing. In: Proc. 19th USENIX Security Symposium (2010)

    Google Scholar 

  4. Berry, D.M.: Abstract appliances and software: the importance of the buyer’s warranty and the developer’s liability in promoting the use of systematic quality assurance and formal methods. Scientific Literature Digital Library and Search Engine (2007), http://www.scientificcommons.org/42749418

  5. Busnelli, F.D., et al.: Principles of European tort law. Springer, Heidelberg (2005)

    Book  Google Scholar 

  6. Dwork, C.: Differential privacy. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 1–12. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  7. Farrell, A.D.H., Sergot, M.J., Sallé, M., Bartolini, C.: Using the event calculus for tracking the normative state of contracts. International Journal of Cooperative Information Systems (IJCIS) 14(2-3), 99–129 (2005)

    Article  Google Scholar 

  8. Fenech, S., Pace, G., Schneider, G.: Automatic Conflict Detection on Contracts. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 200–214. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  9. Fuller, L.L.: The morality of law. Yale University Press, New Haven (1964)

    Google Scholar 

  10. Gössler, G., Le Métayer, D., Raclet, J.-B.: Causality analysis in contract violation. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 270–284. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Goldberg, I.: Privacy-enhancing technologies for the Internet III: Ten years later. In: Digital Privacy: Theory, Technologies, and Practices (2007)

    Google Scholar 

  12. Governatori, G., Milosevic, Z., Sadiq, S.W.: Compliance checking between business processes and business contracts. In: EDOC, pp. 221–232. IEEE, Los Alamitos (2006)

    Google Scholar 

  13. Hildebrandt, M.: Profiling: from data to knowledge. DuD: Datenschutz und Datensicherheit 30(9), 548–552 (2006)

    Article  Google Scholar 

  14. Hildebrandt, M.: Profiling and the rule of law. Identity in the Information Society 1(1), 55–70 (2008)

    Article  Google Scholar 

  15. Jacobs, B.: Architecture is politics: security and privacy issues in transport and beyond. Data Protection in a Profiled World. Springer, Heidelberg (2010)

    Google Scholar 

  16. De Jonge, W., Jacobs, B.: Privacy-friendly electronic traffic pricing via commits. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 143–161. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  17. Kosta, E., Zibuschka, J., Scherner, T., Dumortier, J.: Legal considerations on privacy-enhancing location based services using PRIME technology. Computer Law and Security Report 24, 139–146 (2008)

    Article  Google Scholar 

  18. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Communications of the ACM 21(7), 558–565 (1978)

    Article  MATH  Google Scholar 

  19. Le Métayer, D., Rouvroy, A.: STIC et droit: défis, conflits et complémentarités. Interstices (2008), http://interstices.info/jcms/c_34521/stic--et--droit--defis--conflits--et--complementarites

  20. Le Métayer, D., Monteleone, S.: Automated consent through privacy agents: legal requirements and technical architecture. The Computer Law and Security Review 25(2) (2009)

    Google Scholar 

  21. Le Métayer, D., Maarek, M., Mazza, E., Potet, M.-L., Frenot, S., Viet Triem Tong, V., Crépeau, N., Hardouin, R.: Liability in software engineering: overview of the LISE approach and application on a case study. In: International Conference on Software Engineering, ICSE 2010, pp. 135–144. ACM/IEEE (2010)

    Google Scholar 

  22. Le Métayer, D., Mazza, E., Potet, M.-L.: Designing log architectures for legal evidence. In: 8th International Conference on Software Engineering and Formal Methods, SEFM 2010, pp. 156–165. IEEE, Los Alamitos (2010)

    Chapter  Google Scholar 

  23. Le Métayer, D.: (ed.) Les technologies au service des droits, opportunités, défis, limites. Bruylant, Cahiers du CRID 32 (2010)

    Google Scholar 

  24. Le Métayer, D.: Privacy by design: a matter of choice. Data Protection in a Profiled World, pp. 323–334. Springer, Heidelberg (2010)

    Google Scholar 

  25. Le Métayer, D., Maarek, M., Mazza, E., Potet, M.-L., Frenot, S., Viet Triem Tong, V., Crépeau, N., Hardouin, R.: Liability issues in software engineering. The use of formal methods to reduce legal uncertainties. Communications of the ACM (2011)

    Google Scholar 

  26. Mazza, E., Potet, M.-L., Le Métayer, D.: A formal framework for specifying and analyzing logs as electronic evidence. In: Davies, J. (ed.) SBMF 2010. LNCS, vol. 6527, pp. 194–209. Springer, Heidelberg (2011)

    Google Scholar 

  27. Lessig, L.: The future of ideas: the fate of the commons in a connected world. Random House (2001)

    Google Scholar 

  28. Lessig, L.: Code and other laws of cyberspace, Version 2.0. Basic Books, New York (2007)

    Google Scholar 

  29. OECD guidelines on the protection of privacy and transborder flows of personal data. Organization for Economic Co-operation and Development (1980)

    Google Scholar 

  30. Pace, G.J., Schneider, G.: Challenges in the specification of full contracts. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 292–306. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  31. Poullet, Y.: The Directive 95/46/EC: ten years after. Computer Law and Security Report 22, 206–217 (2006)

    Article  Google Scholar 

  32. Prakken, H., Sergot, M.J.: Contrary-to-duty obligations. Studia Logica 57, 91–115 (1996)

    Article  MATH  Google Scholar 

  33. Prisacariu, C., Schneider, G.: A formal language for electronic contracts. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 174–189. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  34. Reidenberg, J.: Lex informatica: the formulation of information policy rules through technology. Texas Law Review 76, 3 (1998)

    Google Scholar 

  35. Rouvroy, A.: Privacy, data protection and the unprecedented challenges of ambient intelligence. Studies in Ethics, Law and Technology. Berkley Electronic Press (2008)

    Google Scholar 

  36. Ryan, D.J.: Two views on security and software liability. Let the legal system decide. IEEE Security and Privacy (2003)

    Google Scholar 

  37. Steer, S., Craipeau, N., Le Métayer, D., Maarek, M., Potet, M.-L., Viet Triem Tong, V.: Définition des responsabilités pour les dysfonctionnements de logiciels : cadre contractuel et outils de mise en oeuvre. Actes du colloque Droit, sciences et techniques: quelles responsabilités, LITEC, collection Colloques et Débats (2011)

    Google Scholar 

  38. Sweeney, L.: k-anonymity: a model for protecting privacy. Int. J. Uncertain. Fuzziness Knowl.-Based Syst. 10(5), 557–570 (2002)

    Article  MATH  Google Scholar 

  39. Thion, R., Le Métayer, D.: FLAVOR: a formal language for a posteriori verification of legal rules. In: IEEE International Symposium on Policies for Distributed Systems and Networks. IEEE, Los Alamitos (2011)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Grenoble Rhône-Alpes, France

    Daniel Le Métayer

Authors
  1. Daniel Le Métayer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fundación IMDEA Software, Facultad de Informatica (UPM), Campus Montegancedo, 28660, Boadilla del Monte, Madrid, Spain

    Gilles Barthe

  2. Instituto de Computación, Universidad de la República, Facultad de Ingeniería, Julio Herrera y Reissig 565 - Piso 5, 11300, Montevideo, Uruguay

    Alberto Pardo

  3. Department of Computer Science and Engineering, Chalmers | University of Gothenburg, Kunskapsgatan 3, 41756, Gothenburg, Sweden

    Gerardo Schneider

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Le Métayer, D. (2011). Formal Methods as a Link between Software Code and Legal Rules. In: Barthe, G., Pardo, A., Schneider, G. (eds) Software Engineering and Formal Methods. SEFM 2011. Lecture Notes in Computer Science, vol 7041. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24690-6_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-24690-6_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-24689-0

  • Online ISBN: 978-3-642-24690-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation