---
type: Article
title: Formal Methods and Cybersecurity Research
description: Research by James Ortiz on timed automata, temporal logics, model checking, mutation testing, and formal verification of cyber-physical and real-time systems.
resource: https://jamesortiz.site/en/research
tags: [timed-automata, temporal-logics, model-checking, mutation-testing, cybersecurity]
timestamp: 2026-08-15
---

# Research

James Ortiz researches theoretical and applied formal methods: timed automata with asynchronous clocks, temporal and timed logics, model checking, model-based and mutation testing, and verification of cyber-physical and security-critical systems.

## Research topics

### Cyber-Security Systems

Research on formal methods applied to cybersecurity, analyzing security protocols and developing verification techniques for secure systems.

### Cyber-Physical Systems

Modeling and verification of systems that integrate computational and physical processes, ensuring safety and reliability in critical applications.

### Distributed Systems

Modeling and verifying distributed systems, focusing on protocols, algorithms, and formal verification techniques for concurrent systems.

### Real-Time Systems

Research on modeling, verification, and analysis of real-time systems using timed automata and temporal logic specifications.

### Critical Embedded Systems

Developing formal verification techniques for embedded systems in safety-critical domains, ensuring correctness and reliability.

### Timed Automata

Core research on timed automata with partially independent clocks, developing new models and verification algorithms for real-time systems.

### Temporal Logics

Research on temporal logics for specifying and verifying properties of real-time and distributed systems, including TCTL and other temporal formalisms.

### Simulation and Bisimulation

Developing equivalence relations and refinement techniques for timed and distributed systems using simulation and bisimulation theory.

### Model Checking

Applying model checking techniques using tools like UPPAAL and SCADE to verify correctness of real-time and distributed systems.

### Formal Methods

Applying mathematical techniques and formal specifications to design, develop, and verify software and hardware systems with rigorous correctness guarantees.

### Theorem Proving

Research on interactive theorem proving and proof assistants for verifying complex properties of real-time systems and automata models.

### Model-Based Testing

Developing testing methodologies derived from formal models to automatically generate test cases for complex systems and software product lines.

### Mutation Testing

Research on mutation testing techniques for evaluating test suite quality and improving testing effectiveness in highly-configurable systems.

### Software Product Lines

Research on variability modeling, testing highly-configurable systems, and scaling up variability analysis in software product lines.

### Analysis and Symbolic Representation

Developing symbolic techniques and data structures for efficient analysis and verification of large state spaces in timed and distributed systems.

## Related

- [James Ortiz](person.md)
- [Publications](publications.md)
- [Projects](projects.md)
- [Tools](tools.md)