| This dissertation takes place in the larger context of creating automatic tools for identifying errors and enforcing certain properties. From this perspective, we have designed the models and implemented the methods to enforce safety properties in Java-concurrent systems using a supervisory control method.;We have translated the Java original source code to a Petri net to perform the mutual-exclusion analysis. The next step consisted of the generation of a supervisory controller that enforces the mutual-exclusion property and the insertion of the controlled system back to the original code. We have created a novel method for deadlock detection in Java-concurrent programs, including the enforcement of deadlock-prevention policy in these systems by injecting monitors in the original source code. The tests we have performed showed that our methods are feasible and that our techniques are computationally efficient. |
