Kenneth Johnson Auckland University Of Technology

Dr Kenneth Johnson

Senior Lecturer



Email: [email protected]

ORCID: ORCID logo https://orcid.org/0000-0002-9116-7185

Academic appointments:

  • Senior Lecturer, Auckland University of Technology (2013 – ongoing)
  • Postdoctoral Research Fellow, University of York (2010 – 2013)
  • Postdoctoral Researcher, INRIA (2009 – 2010)
  • Research Associate, University of Sheffield (2007 – 2008)

Qualifications:

  • PhD, Swansea University
  • Bachelor of Science, Honours, Computer Science and Mathematics, Carleton University

Overview:

Senior lecturer in the Software Engineering Research Lab (SERL)

I am seeking Post Graduate students (Masters/PhD) for research projects in the following technology areas

Cloud Computing and digital services
Self-adaptive systems
Digital twins
Software tools for disaster management
Social networks
Internet of Things
Graph databases and graph theory
These projects typically involve research in areas relating to formal verification

PhD Candidates should consider applying to one of AUT’s many doctoral scholarships

PG students may also be eligible for a stipend

Students are also welcome to submit their own project proposals

Current Projects:
Efficient Parametric Model Checking: 
www.cs.york.ac.uk/tasp/ePMC/index.html

Probabilistic Verification of Socio-Cyber-Physical Systems: 
serl.aut.ac.nz/resources/probabilistic-verification-of-socio-cyber-physical-systems-of-disaster-affected-regions

Research interests:

Research Areas:
-self-adaptive systems
– probabilistic model checking
– parametric model checking
– socio-cyber-physical systems 
– formal methods for the dependability of cloud-based IT systems
– formal specification, modelling and verification of large-scale IT systems
– algebraic specifications of cloud-based digital services
– algebraic specifications and computation of continuous data types
– graph theory
– social media analysis

Teaching summary:

Programming 2 (Undergraduate)
Introduces the process of program design and implementation using object-oriented programming, with particular emphasis on applications from Computer Science and engineering technology.



Formal Specification & Design (Honours Undergraduate, open to Post-Graduate students)
Introduces formal methods as a collection of mathematical techniques to aid the software engineering process to develop robust systems. Formal methods are applied to case studies via practical model design and specification of engineering artefacts such as data types descriptions, architectures and requirements.



Professional activities:

Featured professional activities
  • QoS of Large-Scale Complex IT Systems, Dagstuhl Seminar Series (19481) (2019 – ongoing)
Editorship, reviewing, examining, and judging
  • Reviewer, ACM Transactions on Software Engineering and Methodology (2020 – ongoing)
  • Reviewer, Journal of Systems and Software (2020 – ongoing)
Invitation to present research
  • Composing Model-Based Analysis Tools (Dagstuhl Seminar 19481), Schloss Dagstuhl, Oktavie-Allee, 66687 Wadern, Germany (2019)
  • Guest Seminar, University of Waikato (2019)

Research outputs:

Featured research outputs
  • Calinescu, R., Paterson, C. A., & Johnson, K. (2019). Efficient parametric model checking using domain knowledge. IEEE Transactions on Software Engineering. doi:10.1109/tse.2019.2912958
  • Calinescu, R., Johnson, K., & Paterson, C. (2018). Efficient Parametric Model Checking Using Domain-Specific Modelling Patterns. In Proceedings of 40th International Conference on Software Engineering (ICSE-NIER 2018) (pp. 61-64). Gothenburg: ICSE. doi:10.1145/3183399.3183404
  • Johnson, K., & Richter, S. (2017). Quantitative verification of social media networks: The case study of Twitter. In Proceedings of the the 4th IEEE/ACM International Conference on Big Data Computing, Applications and Technologies (pp. 53-62). Austin. doi:10.1145/3148055.3148063

Journal articles

  • Calinescu, R., Paterson, C. A., & Johnson, K. (2019). Efficient parametric model checking using domain knowledge. IEEE Transactions on Software Engineering. doi:10.1109/tse.2019.2912958
  • Calinescu, R., Ghezzi, C., Johnson, K., Pezzé, M., Rafiq, Y., & Tamburrelli, G. (2016). Formal verification with confidence intervals to establish quality-of-service properties of software systems. IEEE Transactions on Reliability, 65(1). doi:10.1109/TR.2015.2452931
  • Johnson, K., & Tucker, J. V. (2013). The data type of spatial objects. Formal aspects of computing, 25.

Conference contributions

  • Calinescu, R., Johnson, K., & Paterson, C. (2018). Efficient Parametric Model Checking Using Domain-Specific Modelling Patterns. In Proceedings of 40th International Conference on Software Engineering (ICSE-NIER 2018) (pp. 61-64). Gothenburg: ICSE. doi:10.1145/3183399.3183404
  • Johnson, K., Tucker, J. V., & Wang, V. (2017). Theorising monitoring: Algebraic models of web monitoring in organisations. In Recent Trends in Algebraic Development Techniques WADT 2016. Lecture Notes in Computer Science Vol. 10644 (pp. 13-15). Gregynog: Springer. Retrieved from http://www.springer.com/series/558
  • Calinescu, R., Gerasimou, S., Johnson, K., & Paterson, C. (2017). Using runtime quantitative verification to provide assurance evidence for self-adaptive software: advances, applications and research challenges. In Software Engineering for Self-Adaptive Systems III: Assurances Vol. 9640 LNCS (pp. 223-248). Dagstuhl Castle. doi:10.1007/978-3-319-74183-3_8
  • Johnson, K., & Richter, S. (2017). Quantitative verification of social media networks: The case study of Twitter. In Proceedings of the the 4th IEEE/ACM International Conference on Big Data Computing, Applications and Technologies (pp. 53-62). Austin. doi:10.1145/3148055.3148063
  • Calinescu, R., Johnson, K., & Paterson, C. (2016). FACT: A probabilistic model checker for formal verification with confidence intervals. In TACAS 2016: Lecture Notes in Computer Science Vol. 9636 (pp. 540-546). Eindhoven: Springer Verlag. doi:10.1007/978-3-662-49674-9_32
  • Johnson, K., Sinha, R., Calinescu, R., & Ruan, J. (2015). A multi-agent framework for dependable adaptation of evolving system architectures. In Proceedings of the 41st Euromicro Conference on Software Engineering and Advanced Applications (pp. 159-166). Funchal: IEEE. doi:10.1109/SEAA.2015.49
  • Sinha, R., Johnson, K., & Calinescu, R. (2014). A scalable approach for re-configuring evolving industrial control systems. In Emerging Technology and Factory Automation (ETFA), 2014 IEEE (pp. 1-8). IEEE.
  • Johnson, K., Wang, Y., Calinescu, R., Sommerville, I., Baxter, G., & Tucker, J. V. (2014). Services2Cloud: A framework for revenue analysis of software-as-a-service provisioning. In Cloud Computing Technology and Science (CloudCom), 2013 IEEE 5th International Conference on Vol. 2 (pp. 144-151). Bristol: IEEE. doi:10.1109/CloudCom.2013.117
  • Calinescu, R., Rafiq, Y., Johnson, K., & Bakir, M. E. (2014). Adaptive model learning for continual verification of non-functional properties. In Proceedings of the 5th ACM/SPEC international conference on Performance engineering (pp. 87-98). Dublin: ACM. doi:10.1145/2568088.2568094
  • Sinha, R., Johnson, K., & Calinescu, R. (2014). A scalable approach for re-configuring evolving industrial control systems. In Proceedings of the 2014 Emerging Technology and Factory Automation (ETFA) Vol. 19 (pp. 1-8). Barcelona: IEEE. doi:10.1109/ETFA.2014.7005126
  • Johnson, K., & Calinescu, R. (2014). Efficient re-resolution of SMT specifications for evolving software architectures. In Proceedings of the 10th international ACM Sigsoft conference on Quality of software architectures (pp. 93-102). Marcq-en-Bareul. doi:10.1145/2602576.2602578
  • Johnson, K., Calinescu, R., & Kikuchi, S. (2013). An incremental verification framework for component-based software systems. In CBSE ’13 Proceedings of the 16th International ACM Sigsoft Symposium on Component-Based Software Engineering (pp. 33-42). Vancouver, British Columbia: ACM. doi:10.1145/2465449.2465456
  • Johnson, K., & Tucker, J. V. (2013). Algebraic specifications of computing as a service with applications to cost analysis. In Proceedings of the 2012 IEEE/ACM Fifth International Conference on Utility and Cloud Computing Vol. 2 (pp. 144-151). IEEE Computer Society. doi:10.1109/UCC.2012.46
  • Calinescu, R., Johnson, K., Rafiq, Y., Gerasimou, S., Silva, G. C., & Pehlivanov, S. N. (2013). Continual Verification of Non-Functional Properties in Cloud-Based Systems.(Invited Paper). In NiM-ALP@ MoDELS Vol. 1074 (pp. 1-5). Miami, USA: CEUR. Retrieved from http://ceur-ws.org/Vol-1074/
  • Calinescu, R., Johnson, K., & Rafiq, Y. (2013). Developing self-verifying service-based systems. In Proceedings of the ASE-2013: The 28th The 28th IEEE Conference on Automated Software Engineering ACM/IEEE (pp. 734-737). Silicon Valley: IEEE. doi:10.1109/ASE.2013.6693145
  • Calinescu, R., Kikuchi, S., & Johnson, K. (2012). Compositional reverification of probabilistic safety properties for large-scale complex IT systems. In Lecture Notes in Computer Science Vol. 7539 (pp. 303-329). Oxford: Springer Verlag. doi:10.1007/978-3-642-34059-8_16
  • Johnson, K., Reed, S., & Calinescu, R. (2011). Specification and quantitative analysis of probabilistic cloud deployment patterns. In Unknown Conference (pp. 145-159). Springer. doi:10.1007/978-3-642-34188-5_14
  • Calinescu, R., Johnson, K., & Rafiq, Y. (2011). Using observation ageing to improve Markovian model learning in QoS engineering. In Proceedings of the 2nd ACM/SPEC International Conference on Performance engineering (pp. 505-510). ACM. doi:10.1145/1958746.1958823
  • Johnson, K., Besnard, L. I., Gautier, T., & Talpin, J. -P. (2010). 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010). .
  • Besnard, L. I., Gautier, T., Moy, M., Talpin, J. -P., Johnson, K., & Maraninchi, F. (2009). Automatic translation of C/C++ parallel code into synchronous
    formalism using an SSA intermediate form. In PreProceedings of t he Ninth International Workshop on Automated Verification of Critical Systems (pp. 77-92). Swansea. Retrieved from http://www.cs.swan.ac.uk/avocs09/PreProceedings.pdf [PDF]
  • Besnard, L., Gautier, T., Moy, M., Talpin, J. -P., Johnson, K., & Maraninchi, F. (2009). Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form. .
  • Walkinshaw, N., Bogdanov, K., & Johnson, K. (2008). Evaluation and comparison of inferred regular grammars. In ICGI ’08: Proceedings of the 9th international colloquium on Grammatical Inference: Algorithms and Applications (pp. 252-265). Saint-Malo: Springer. doi:10.1007/978-3-540-88009-7_20

Reports

  • Calinescu, R., Johnson, K., & Rafiq, Y. (2013). University of York Technical Report YCS-2013-484.
  • Johnson, K., Besnard, L., Gautier, T., & Talpin, J. -P. (2010). A Synchronous Approach to Threaded Program Verification (7320). Retrieved from https://hal.inria.fr/inria-00492694v2/document

Software

Theses

  • Johnson, K. H. A. (2007). The algebraic specification of spatial data types with applications to constructive volume geometry. (Swansea University).

Oral presentations

  • Johnson, K. (2019). Efficient parametric model checking using domain knowledge. Hamilton, New Zealand. Retrieved from https://cms.its.waikato.ac.nz/
  • Johnson, K. (2015). Formal Methods in the Cloud. Limassol, Cyprus.
  • Johnson, K. (2015). A Multi-Agent Framework for Dependable Adaptation of Evolving System Architectures. Funchal, Portugal.
  • Johnson, K. (2014). Efficient Re-resolution of SMT Specifications for Evolving Software Architectures. Lille, France.
  • Johnson, K. (2014). Efficient Re-resolution of SMT Specification for Evolving Software Architectures. AUT.
  • Johnson, K., Calinescu, R., & Kikuchi, S. (2013). An incremental verification framework for component-based software systems. ACM.
  • Johnson, K. (2012). Algebraic Specifications of Computing as a Service with Applications to Cost Analysis. Chicago.
  • Johnson, K. (2012). Incremental Verification with Applications to Cloud Deployments. Edinburgh.
  • Johnson, K. (2012). A Model of Computing as a Service for Cost Analysis. Cambridge University.
  • Johnson, K. (2012). Formal Methods for Cloud Computing Technologies. Swansea, UK.
  • Johnson, K. (2012). Automated Management of Cloud Infrastructures. Windermere, UK.
  • Johnson, K. (2011). Cost Analysis of Cloud Computing Services. London.
  • Johnson, K. (2011). Cloud Computing. Birmingham.
  • Johnson, K. (2011). Automated Management of Cloud Infrastructures. Bristol.
  • Johnson, K. (2010). A Synchronous Approach to Threaded Program Verification – Presentation of a paper at the Automated Verification of Critical Systems conference. Düsseldorf, Germany.
  • Johnson, K. (2009). Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form. Swansea, UK.
  • Johnson, K. (2009). Continuous Data Types and Computation. Saint- Jacut-de-la-Mer, France.